[afflom]

What it does

The proof form the maintainer chose on #91 (option B, comment 6285275601) for the runtime profile's refinement statements, stacked on PR 2a (#227).

term_cases{scrutinee: <document term>, definitions: [<prior definitions>]}, language 1.2 only. It lowers to

cases llCase : <term> <;>
  simp (config := {decide := true}) only [<definitions>, llCase]

• The term's type must be an inductive type of the document; the list is nonempty, strictly sorted and duplicate-free, each a prior document definition; llCase is reserved. No tactic name, option, or lemma is free.
• SemanticProof::TermCases in ir/semantic.rs (validation check_term_cases, node count, term visitors, widening, binder/type-argument walks), the Lean lowering in backend/semantic.rs, and the two v2 schemas (semantic-module-v2, semantic-snapshot-v2: three oneOf entries). The notation reads the form from the schema, so the formatter and notation round trip need no code. The v1 schemas are untouched, so language 1.1 cannot carry it.
• SPEC §17.10 states why it is admitted and what axioms it draws on; SM-35 register row, scenario and conformance_sm_35, in R3 order (row commit first). Register 430 on this draft (the maintainer assigns the final count).

Measured

• conformance_sm_35: the project links; semantic-module-v2 accepts the module; the formatter keeps the proof and its fixed point links to the same module; the notation reads back to the same module; the generated Lean has the stated lowering; the pinned Lean 4.32.1 verifies the module with exactly [propext]; seven misuses are refused as LLT4001 naming the misuse (language 1.1, empty list, out of order, repeated, absent definition, a Nat term, a parameter named llCase). Three plants caught (VERIFICATION.md).
• The motivating proof: on the nat_add slice (not in this PR) the same script proves runExport … = runItem … for all operands in six seconds with propext, Classical.choice, Quot.sound.
• fmt, clippy -D warnings, validate-model (430), validate-spec-links (430), check-test-inventory (758), the bdd meta-gate: clean.
• semantic-ir, proofs and declarations suites (76 cases): 54 pass, 22 fail, all 22 with LLC0102 (the lock is bound to the compiler-semantics ID, which has moved since PR 1); none on the schema, the proof forms or the snapshot. I did not rerun them on the base.
• cargo test -p lexlean: 207 of 208 pass; the failure is the rust_renderer record.

Two things to know

1. There is no LaTeX phrase to add. The canonical LaTeX of a semantic module is a catalog of declarations: for a theorem it states kind, parameters, statement and axiom policy, and no proof for any form (observed on the output of the case). §19.5's phrases are for the document language's proofs. The case asserts the catalog carries the theorem and does not mention term_cases; condition 2 of the decision assumed a proof phrase, so this needs your reading.
2. The negative cases are planted projects inside the case, not committed fixtures under tests/negative/. A committed fixture carries a lock and expected diagnostics bound to the compiler-semantics ID, which the wave regenerates; the case plants the same misuses and asserts each refusal, without files that go stale. Say if you want committed fixtures after the wave.

Not run / left for the wave

Records bound to the compiler-semantics ID, check-calculus, full just vv, other hosts, repro, honesty. One plant not shown: whether the pinned Lean also rejects a lowering without llCase in the simp list (the case's lowering assertion catches it first).

---

Generated by Claude Code

[afflom]

Amendment c44c469 reviewed: accepted. set_option linter.unusedSimpArgs false in on the generated cases … <;> simp only script is a scoped script setting, not an R8 bypass: the lowering is fixed text with no user-supplied tactic, option or lemma (backend/semantic.rs:1284); it is necessary because verify refuses any Lean output (LLV7006) and a superset definition list trips the unused-simp-argument lint on every term_cases proof; it cannot hide an unused hypothesis (linter.unusedVariables is untouched, the kernel checks the term, the policy audits the axioms); ite_true/ite_false are plain rfl simp lemmas with no axioms; the same file already does it at :1468. Stated in SPEC §17.10 with the reason, in the SM-35 statement, asserted by the case, recorded in VERIFICATION with the failure it fixes. conformance_sm_35 passes on the stack's head.

---

Generated by Claude Code

[afflom]

Maintainer: landed on release/v0.4 by #248 (merge commit 9796067, the #91 stage-4 stack regenerated on one compiler-semantics identity, full gate green on 677e88d). Closing by hand, since release-line merges do not auto-close.

---

Generated by Claude Code