proof(L2): hybrid — has_type_l1 m-indexed + Modality.v + linear_to_affine Qed (zero axioms)#176

Merged

hyperpolymath merged 14 commits into

mainfrom

May 27, 2026

proof+design: verified counterexample to preservation + four-layer redesign

hyperpolymath
and
claude
committed
proof(L1): typing judgment with R-threading + counterexample regression Qed (#155)

hyperpolymath
and
claude
authored
proof(L1): Semantics_L1.v skeleton — preservation_l1 theorem stated (#157)

hyperpolymath
and
claude
authored
proof(L1.A): value_R_G_preserving_l1 Qed (#158)

hyperpolymath
and
claude
authored
proof(L1.B): region_shrink_preserves_typing_l1 Qed via _gen helper (#159)

hyperpolymath
and
claude
authored
proof(L1.C): subst_preserves_typing_l1 Qed (with strengthened statement) (#160)

hyperpolymath
and
claude
authored
proof(L1.D): preservation_l1 body — 29/33 cases closed, 4 admits surface R-weakening gap (#161)

hyperpolymath
and
claude
authored

Provide feedback