proof: add structural WithInternals head witnesses

[Th0rgal]

Base / dependency

Stacked on PR #2112 (paloma/issue-2080-structural-withinternals). Do not merge until predecessor stack is merged/green.

Predecessor stack observed before PR creation:

• proof: make scope lift helper-world parametric #2108 open, mergeable
• proof: add direct helper WithInternals interfaces #2111 open, mergeable
• proof: add structural helper WithInternals assembly #2112 open, mergeable, checks green

Summary

• Adds a structural-only StmtListGenericWithHelpersAndHelperIRWithInternals assembly bridge for lists whose heads are all structural helper-recursive heads.
• Adds concrete WithInternals structural head witnesses for Stmt.ite and Stmt.forEach, packaging exact CompiledStmtStepWithHelpersAndHelperIRWithInternals head steps into the phase-17 structural interface without falling back to the legacy/default-empty helper-world list seam.
• Regenerates PrintAxioms.lean for the two new public theorem names.

Validation

• lean-slot lake build Compiler.Proofs.HelperStepProofs - passed
• lean-slot lake build Compiler.Proofs.IRGeneration.GenericInduction.InterfaceAssembly - passed
• python3 scripts/generate_print_axioms.py --check - passed
• python3 scripts/check_proof_length.py - passed (5729 proofs scanned; no new proofs exceed hard limit)
• git diff --check - passed
• rg -n "\b(sorry|admit|axiom)\b" Compiler/Proofs/HelperStepProofs.lean Compiler/Proofs/IRGeneration/GenericInduction/InterfaceAssembly.lean - no matches

Remaining #2080 interface/gate

This narrows the structural recursive-head packaging, but it does not yet prove full structural ite/forEach preservation from nested StmtListGenericWithHelpersAndHelperIRWithInternals bodies. The next gate remains adding/using the WithInternals execution sibling for the helper-IR generic list theorem so body-level/function-level preservation can consume the mixed WithInternals list witness directly and continue reducing reliance on SupportedStmtList.helperSurfaceClosed.

Refs #2080

---

Note

Low Risk
Lean proof-only additions (inductive packaging and thin wrappers); no compiler runtime, auth, or execution semantics changes.

Overview
Extends the phase-17 WithInternals helper-proof plumbing so structural recursive heads (Stmt.ite, Stmt.forEach) can be wired without the legacy empty-internal-functions compile path.

HelperStepProofs adds two thin lemmas that take an exact CompiledStmtStepWithHelpersAndHelperIRWithInternals head step and a structural tail witness, then build StmtListStructuralInternalHelperStepInterfaceWithInternals for ite :: rest and forEach :: rest (both delegate to the existing cons_of_compiledStep lemma).

InterfaceAssembly adds stmtListGenericWithHelpersAndHelperIRWithInternals_of_structuralInternalHelperStepInterfaceWithInternals, mirroring the expression- and direct-helper list bridges: when every statement in the list is a structural helper head, the structural interface inductively assembles into StmtListGenericWithHelpersAndHelperIRWithInternals.

PrintAxioms.lean is regenerated to register the two new public theorem names (+2 public lemmas in the inventory).

^{Reviewed by Cursor Bugbot for commit 1cbc08a. Bugbot is set up for automated code reviews on this repo. Configure here.}

[vercel]

The latest updates on your projects. Learn more about Vercel for GitHub.

Project	Deployment	Actions	Updated (UTC)
verity	Ready	Preview, Comment	Jul 7, 2026 12:34am

[cursor]

Bugbot couldn't run - usage limit reached

Bugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit.

A user or team admin can review and increase usage limits in the Cursor dashboard.

(requestId: serverGenReqId_70d0d6c3-753b-4205-9509-3d10b59094d2)

[Th0rgal]

Scoped review of #2113 found no code-level blocker in the single-commit diff (1cbc08a): the new structural WithInternals head packaging mirrors the existing generic cons witness, the structural-only list bridge matches the direct/expr bridge shape, PrintAxioms.lean is in sync, git diff --check passed, proof-length check passed, and no new sorry/admit/axiom was found in the touched proof files.

Not merging yet:

• CI is still pending on downstream jobs for this PR.
• This PR is stacked on proof: add structural helper WithInternals assembly #2112, with predecessor stack proof: make scope lift helper-world parametric #2108 -> proof: add direct helper WithInternals interfaces #2111 -> proof: add structural helper WithInternals assembly #2112 still open; per merge policy, proof: add structural WithInternals head witnesses #2113 should wait until the predecessor stack is merged/green.
• Cursor Bugbot did not run because the usage limit was reached, but there are no PR review threads.

Next action: wait for #2113 CI to finish green, merge the predecessor stack first, then recheck and merge #2113.

Exact blocker: #2113 CI is still pending and predecessor PRs #2108/#2111/#2112 are still open.