Repository navigation

proof(L2): complete L2-modality migration of L1 preservation (Stage A); soundness fix to follow - #294

Merged

hyperpolymath merged 13 commits into

mainfrom

proof/l1-soundness-modality-thread

Jun 15, 2026

Merged

proof(L2): complete L2-modality migration of L1 preservation (Stage A); soundness fix to follow#294
hyperpolymath merged 13 commits into
mainfrom
proof/l1-soundness-modality-thread

Commits on May 26, 2026
- proof+design: verified counterexample to preservation + four-layer redesign
  
  hyperpolymath
  and
  claude
  committed
  06e344f
- proof(L1): typing judgment with R-threading + counterexample regression Qed (#155)
  
  hyperpolymath
  and
  claude
  authored
  1e9d40f
- proof(L1): Semantics_L1.v skeleton — preservation_l1 theorem stated (#157)
  
  hyperpolymath
  and
  claude
  authored
  1e45e3f
- proof(L1.A): value_R_G_preserving_l1 Qed (#158)
  
  hyperpolymath
  and
  claude
  authored
  c6b1cda
- proof(L1.B): region_shrink_preserves_typing_l1 Qed via _gen helper (#159)
  
  hyperpolymath
  and
  claude
  authored
  9b9f3fe
- proof(L1.C): subst_preserves_typing_l1 Qed (with strengthened statement) (#160)
  
  hyperpolymath
  and
  claude
  authored
  65d665e
- proof(L1.D): preservation_l1 body — 29/33 cases closed, 4 admits surface R-weakening gap (#161)
  
  hyperpolymath
  and
  claude
  authored
  d0c5117
Commits on May 27, 2026
Commits on Jun 15, 2026
- proof(L2): complete L2-modality migration of L1 preservation development
  
  hyperpolymath
  and
  claude
  committed
  d2baf75
- merge: resolve conflicts and fix headers
  hyperpolymath
  committed
  49cac03