max
0 followers · 0 following
  • Joined on 2026-04-25
Repositories
7
 Projects Packages Public activity Starred repositories
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 16:56:05 -05:00
825d8af68d Layer 0 substrate round 6: contract auto-registration
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 16:19:43 -05:00
294e96633d Layer 0 substrate round 5: Tactic/EqContract.lean + barrel + Ω-call fixes
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 15:51:32 -05:00
2f343b0980 Layer 0 substrate round 4: Reflect.lean — bidirectional CTerm/CType ↔ Lean.Expr
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 15:05:02 -05:00
7ca4ac8d6a Omega.lean: upgrade operators to use CTerm.code (engine universe-code)
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 10:45:18 -05:00
5de7d9e7d0 Layer 0 substrate round 3: Contract.lean — topos-internal contract framework
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 10:26:58 -05:00
7934275f68 Layer 0 substrate round 2: Subobject + SIP + Modality + Bridge/Set
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-05 10:11:31 -05:00
f6231f3e64 Layer 0 substrate (Truncation, Decidable, Omega, Category, Reify)
max pushed to master at max/infoductor 2026-05-05 08:34:17 -05:00
c995d4b323 Foundation: structural Lean.Syntax bidirectional reflection
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-04 01:22:44 -05:00
19928d040a REL2 universe stratification + topolei naming cleanup + Rust ABI v4
max pushed to master at max/infoductor 2026-05-01 14:15:35 -05:00
e908fc442f Document Phase 3 proof plan in docs/PHASE3_PROOF_PLAN.md
max pushed to master at max/infoductor 2026-05-01 14:12:40 -05:00
665046a353 Phase 3 Lean 4.30 String-internals analysis
max pushed to master at max/infoductor 2026-05-01 14:03:53 -05:00
62b73bb176 Atomic Phase 3 witnesses via decide
max pushed to master at max/infoductor 2026-05-01 14:01:39 -05:00
6b9ac691cb Phase 3 foundation lemmas; full universal documented
max pushed to master at max/infoductor 2026-05-01 13:50:34 -05:00
8733a6ff89 Universal round-trip theorems at the token level
max pushed to master at max/infoductor 2026-05-01 13:28:56 -05:00
9c9b93c3ca Fuel-based parsers + kernel-level round-trip via decide
max pushed to master at max/infoductor 2026-05-01 13:20:05 -05:00
92fc4f9682 Add String → MetaCTerm parser; round-trip via native_decide
max pushed to master at max/infoductor 2026-05-01 13:05:44 -05:00
ae675a1eed Add MetaCTerm/MetaClassifier/MetaArtifact source renderer
max pushed to master at max/infoductor 2026-05-01 10:08:25 -05:00
511d564a55 Add MetaCTerm structural mirror, .cterm artifact arm, MetaPosition.binder
max pushed to Dev_REL2 at max/cubical-transport-hott-lean4 2026-05-01 08:53:01 -05:00
d03746497b Drop Infoductor dependency; cubical-transport is now pure cubical engine
max pushed to master at max/infoductor 2026-05-01 08:39:43 -05:00
f4787b9091 Phase B: Comonad sub-library — proof-pattern detection ported from mm-lean