proof: Lemma B at-pre helpers Qed + preservation Phase 2 wired (12→11 admits)#146

Merged

hyperpolymath merged 15 commits into

mainfrom

lemma-b-phase2

May 26, 2026

Commits on May 26, 2026

docs(audit): reconcile standards#134 sub-tasks against 2026-05-26 ground truth

hyperpolymath
and
claude
committed
docs(handoff): correct case counts after 2026-05-24 cluster closures

hyperpolymath
and
claude
committed
docs(audit): Lemma B Phase 2 Option 2 hits a real obstacle, pivot to Option 1

hyperpolymath
and
claude
committed
docs: session note + STATE.a2ml refresh for the Lemma B pivot

hyperpolymath
and
claude
committed
docs: ROADMAP + PROOF-NEEDS reflect 2026-05-26 Path-1 pivot

hyperpolymath
and
claude
committed
proof: Qed step_preserves_type + step_output_context_eq via at-pre helpers
hyperpolymath
committed
proof: close 27 of 35 cases in step_preserves_type_at_pre via copied tactic blocks
hyperpolymath
committed
proof: copy step_output_context_eq's tactic blocks into _at_pre helper
hyperpolymath
committed
docs(proof-needs): Path 3 (at-pre helper) closes the shared 4885/5963 admit
hyperpolymath
committed
proof: swarm A+B integration — 3 more cases closed in at-pre helpers + docs
hyperpolymath
committed
proof: scaffold S_Let_Step LEFT splice with idtac RIGHT fallthrough
hyperpolymath
committed
proof: Swarm A+B+C closures land — at-pre helpers Qed, 10 preservation LEFT branches closed

hyperpolymath
and
claude
committed
docs: ROADMAP + PRESERVATION-HANDOFF reflect at-pre helpers Qed (post d6ebf68)

hyperpolymath
and
claude
committed
proof: narrow MIDDLE branches in preservation S_*_Step blocks (10 admits → pop-only)

hyperpolymath
and
claude
committed
proof: typing_free_of_absent_region (Qed) — Brief C kernel (#151)

hyperpolymath
and
claude
authored

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

proof: Lemma B at-pre helpers Qed + preservation Phase 2 wired (12→11 admits)#146

proof: Lemma B at-pre helpers Qed + preservation Phase 2 wired (12→11 admits)#146
hyperpolymath merged 15 commits into
mainfrom
lemma-b-phase2

Commits on May 26, 2026

docs(audit): reconcile standards#134 sub-tasks against 2026-05-26 ground truth

docs(handoff): correct case counts after 2026-05-24 cluster closures

docs(audit): Lemma B Phase 2 Option 2 hits a real obstacle, pivot to Option 1

docs: session note + STATE.a2ml refresh for the Lemma B pivot

docs: ROADMAP + PROOF-NEEDS reflect 2026-05-26 Path-1 pivot

proof: Qed step_preserves_type + step_output_context_eq via at-pre helpers

proof: close 27 of 35 cases in step_preserves_type_at_pre via copied tactic blocks

proof: copy step_output_context_eq's tactic blocks into _at_pre helper

docs(proof-needs): Path 3 (at-pre helper) closes the shared 4885/5963 admit

proof: swarm A+B integration — 3 more cases closed in at-pre helpers + docs

proof: scaffold S_Let_Step LEFT splice with idtac RIGHT fallthrough

proof: Swarm A+B+C closures land — at-pre helpers Qed, 10 preservation LEFT branches closed

docs: ROADMAP + PRESERVATION-HANDOFF reflect at-pre helpers Qed (post d6ebf68)

proof: narrow MIDDLE branches in preservation S_*_Step blocks (10 admits → pop-only)

proof: typing_free_of_absent_region (Qed) — Brief C kernel (#151)