Commit graph

  • c995d4b323 Foundation: structural Lean.Syntax bidirectional reflection master Maximus Gorog 2026-05-05 07:33:42 -06:00
  • e908fc442f Document Phase 3 proof plan in docs/PHASE3_PROOF_PLAN.md Maximus Gorog 2026-05-01 13:15:32 -06:00
  • 665046a353 Phase 3 Lean 4.30 String-internals analysis Maximus Gorog 2026-05-01 13:12:38 -06:00
  • 62b73bb176 Atomic Phase 3 witnesses via decide Maximus Gorog 2026-05-01 13:03:51 -06:00
  • 6b9ac691cb Phase 3 foundation lemmas; full universal documented Maximus Gorog 2026-05-01 13:01:38 -06:00
  • 8733a6ff89 Universal round-trip theorems at the token level Maximus Gorog 2026-05-01 12:50:31 -06:00
  • 9c9b93c3ca Fuel-based parsers + kernel-level round-trip via decide Maximus Gorog 2026-05-01 12:28:55 -06:00
  • 92fc4f9682 Add String → MetaCTerm parser; round-trip via native_decide Maximus Gorog 2026-05-01 12:20:03 -06:00
  • ae675a1eed Add MetaCTerm/MetaClassifier/MetaArtifact source renderer Maximus Gorog 2026-05-01 12:05:43 -06:00
  • 511d564a55 Add MetaCTerm structural mirror, .cterm artifact arm, MetaPosition.binder Maximus Gorog 2026-05-01 09:08:01 -06:00
  • f4787b9091 Phase B: Comonad sub-library — proof-pattern detection ported from mm-lean Maximus Gorog 2026-05-01 07:39:36 -06:00
  • ba0a49823b Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries Maximus Gorog 2026-05-01 07:20:36 -06:00