Merge pr 125 - #128

Merged

hyperpolymath merged 16 commits into

mainfrom

May 24, 2026

Commits on May 24, 2026

proof(coq): Phase 1 — cfg-remember + atomic-axiom tactic on Lemma B (4 of 35 closed)
claude
committed
proof(coq): add subst_preserves_typing_strong (unlocks Cluster A of Lemma B)
claude
committed
proof(coq): Qed output_ctx_det — output-context determinacy for has_type
claude
committed
proof(coq): Lemma B — close 3 Cluster A cases (S_Let_Val, S_LetLin_Val, S_App_Fun)
claude
committed
proof(coq): Lemma B — close all 7 Cluster A cases (S_If_True/False, S_Case_Inl/Inr)
claude
committed
proof(coq): Lemma B — close 4 Cluster C cases (S_Fst, S_Snd, S_Copy, S_Region_Exit)
claude
committed
proof(coq): Lemma B — close 10 Cluster B congruence cases (35->11, 69%)
claude
committed
proof(coq): close S_App_Step1, S_App_Step2 via sibling type_determinacy; ctx_types_agree sym/trans
claude
committed
proof(coq): Lemma B — Cluster C complete (S_StringLen atomic, S_Region_Enter)
claude
committed
proof(coq): introduce step_preserves_type sub-lemma (partial; ~15 of 35 cases closed)
claude
committed
proof(coq): step_preserves_type clone-out — 8 more cases (12 of 35 remain)
claude
committed
proof(coq): step_preserves_type — close 4 cases fully, structure remaining 8 with LEFT branch closed
claude
committed
proof(coq): step_preserves_type — add step_R_change_shape, close MIDDLE branches
claude
committed
proof(coq): step_preserves_type — close 7 RIGHT sub-cases via membership-eq + perm
claude
committed
Merge branch 'pr-125' into merge-pr-125
hyperpolymath
committed
Merge branch 'main' into merge-pr-125
hyperpolymath
authored