Repository navigation

Proof/l2 modality hybrid - #215

Closed

hyperpolymath wants to merge 15 commits into

mainfrom

proof/l2-modality-hybrid

Closed

Proof/l2 modality hybrid#215
hyperpolymath wants to merge 15 commits into
mainfrom
proof/l2-modality-hybrid

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