Actor
max
Status
Layer 3.3a: substantive unit/counit + typed-correctness for adjoint triple
lean_action_ci.yml #43 -Commit
391a048dcf
pushed by
max
Axiom debt cleanup: discharge or convert all 99 engine axioms
lean_action_ci.yml #42 -Commit
0a7228a8e5
pushed by
max
Refactor Phase 4: Rust ABI v6 → v7 (modal tag unification)
lean_action_ci.yml #41 -Commit
567d8722d5
pushed by
max
Refactor Phase 3a: Modal.lean rewrite — forModalityKind unification
lean_action_ci.yml #40 -Commit
cfabca3404
pushed by
max
Refactor Phase 2: modal unification — Lean engine cascade
lean_action_ci.yml #39 -Commit
6e4936d6ee
pushed by
max
Remove Test/Reify.lean — Phase 1 macro-debugging scratch
lean_action_ci.yml #38 -Commit
c334bf9784
pushed by
max
Refactor Phase 1: derive_reflect_reify macro — Reflect.lean elegance pass
lean_action_ci.yml #37 -Commit
2417ec667b
pushed by
max
Modal cascade Phase 3: Modal.lean module proper — Layer 0 complete
lean_action_ci.yml #36 -Commit
c7f91fa933
pushed by
max
Modal cascade Phase 2: Rust ABI v5 → v6 (modal constructors)
lean_action_ci.yml #35 -Commit
c6bc0aa68f
pushed by
max
Modal cascade Phase 1: Syntax + Lean engine cascade
lean_action_ci.yml #34 -Commit
b9ca1d8875
pushed by
max
Layer 0 substrate round 6: contract auto-registration
lean_action_ci.yml #33 -Commit
825d8af68d
pushed by
max
Layer 0 substrate round 5: Tactic/EqContract.lean + barrel + Ω-call fixes
lean_action_ci.yml #32 -Commit
294e96633d
pushed by
max
Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr
lean_action_ci.yml #31 -Commit
2f343b0980
pushed by
max
Omega.lean: upgrade operators to use CTerm.code (engine universe-code)
lean_action_ci.yml #30 -Commit
7ca4ac8d6a
pushed by
max
Layer 0 substrate round 3: Contract.lean — topos-internal contract framework
lean_action_ci.yml #29 -Commit
5de7d9e7d0
pushed by
max
Layer 0 substrate round 2: Subobject + SIP + Modality + Bridge/Set
lean_action_ci.yml #28 -Commit
7934275f68
pushed by
max
Layer 0 substrate (Truncation, Decidable, Omega, Category, Reify)
lean_action_ci.yml #27 -Commit
f6231f3e64
pushed by
max
REL2 universe stratification + topolei naming cleanup + Rust ABI v4
lean_action_ci.yml #26 -Commit
19928d040a
pushed by
max
Drop Infoductor dependency; cubical-transport is now pure cubical engine
lean_action_ci.yml #25 -Commit
d03746497b
pushed by
max
Extract Algebra/ foundation to Infoductor; require it from forgejo
lean_action_ci.yml #24 -Commit
e26ada2fbc
pushed by
max
Drop algebra-restructure exe — source code IS the CLI
lean_action_ci.yml #23 -Commit
de56626059
pushed by
max
Abstract the four ⚠️ tools into well-defined primitives
lean_action_ci.yml #22 -Commit
48b7326523
pushed by
max
algebra-restructure CLI + asyncMode .sync on registries
lean_action_ci.yml #21 -Commit
b88f6e6f62
pushed by
max
EngineMethodologies + cubical_close: ALGEBRA §9 closer set
lean_action_ci.yml #20 -Commit
333f31d4bc
pushed by
max
@[metaPath] + structured failure + engine-bound methodologies
lean_action_ci.yml #19 -Commit
60f7ecdf54
pushed by
max
ALGEBRA Phases A+B+C+D' + cubical_search tactic + doc state-of-play
lean_action_ci.yml #18 -Commit
7ccebb606d
pushed by
max
QUESTIONS Levels 1.5 + 2: full DecidableEq + simp routing
lean_action_ci.yml #17 -Commit
271b47102e
pushed by
max
QUESTIONS Level 1: CompQ reified + classifier-conditioned axioms
lean_action_ci.yml #16 -Commit
6adbce0c1b
pushed by
max
Document the question-form algebra + Dev_Algebra plan + Eulerian record
lean_action_ci.yml #15 -Commit
95f11020d7
pushed by
max
REL2 Phase 2: Bridge.lean — Eq ↔ Path interop
lean_action_ci.yml #14 -Commit
7152807b66
pushed by
max