[humuhumu33]

Fixes #280 on the v0.4 line. term_cases and SM-35 exist only on release/v0.4 (release/v0.5 stops at SM-34 and has had no forward merge since 9989278), so this targets release/v0.4; say if you want it on another line.

term_cases could not close a case that equates two constructors over a variable. Its simp only set decided closed propositions only. It now names Lean's no-confusion procedure, the injectivity lemmas, and the propositional units those leave. The set stays fixed and closed: every rule is written in the script, and none comes from simp's default set.

The lowering (SPEC §17.10, SM-35)

Before:

set_option linter.unusedSimpArgs false in cases llCase : <term> <;> simp (config := {decide := true}) only [<definitions>, llCase, ite_true, ite_false]

After:

set_option linter.unusedSimpArgs false in cases llCase : <term> <;> simp (config := {decide := true}) only [<definitions>, llCase, ite_true, ite_false, reduceCtorEq, false_implies, imp_self, and_true, true_and, Option.some.injEq, Except.error.injEq, Except.ok.injEq, List.cons.injEq, <injectivity>]

Here <injectivity> is <T>.<c>.injEq for every constructor c with at least one field of every inductive type T the module declares, in declaration order.

The rules do this:

• reduceCtorEq rewrites an equation between two different constructors to False.
• Each injEq lemma rewrites an equation between two applications of one constructor to the equations of their fields. Lean generates one for every constructor with a field.
• false_implies, imp_self, and_true and true_and close the implication and the conjunction those rewrites leave.

The backend change is in crates/lexlean/src/backend/semantic.rs. It adds the fixed TERM_CASES_RULES and gives Render the module's constructors that have a field.

Register (R3)

There is no new row. SM-35 is amended in model/ids.toml, the SPEC §31 table, the scenario, and CONFORMANCE.md, which is regenerated. The amended statement:

… then simp only over the named definitions, that hypothesis, the reduction of a conditional on a decided condition, the refutation of an equation between two different constructors, the injectivity equation of every constructor with a field of Option, Result, List, and each inductive type the module declares, and the fixed rules that close an implication from False or of a proposition by itself and drop True from a conjunction, with closed propositions decided, which uses exactly the axioms the theorem's policy states, so a theorem whose cases need constructor disjointness or injectivity verifies and a false one is rejected by Lean; …

The register count is unchanged, so README needs no edit for RP-11. Forward merge: the amended SM-35 text, the §17.10 paragraph, and the backend change must be carried into release/v0.5 with term_cases itself on the next forward merge.

The commits are in order:

• fa9c7c1 holds the row text, the scenario and the failing case. The case fails on the unchanged lowering at the generated rule list.
• 1282b38 holds the lowering.
• bf237cb holds the VERIFICATION record and CHANGELOG.
• 0cf8986 merges release/v0.4 902d7de.

The case

conformance_sm_35 keeps its existing project and builds four more from the issue's module:

Project	Needs	Pinned Lean
The issue's module, check n = bad p → report n = some p	disjointness and injectivity of Verdict and Option	verifies, [propext]
report n = none → check n = good	an Option disjointness in the hypothesis	verifies, [propext]
check n = bad p → paired n = Pair.mk 0 p	injectivity of a two-field constructor, true_and	verifies, [propext]
check n = bad p → report n = none, which is false	nothing	rejected, LLV7002, ⊢ x✝ = p → False

The first cut lacked false_implies. The two-field project then left ⊢ False → 0 = p open, so the rule and the text now name it.

Plants (VERIFICATION.md)

Each plant was one edit, restored by git checkout. Each turns conformance_sm_35 red. Each was also run through lexlean verify on the four projects, and the real Lean output is in the record.

1. The old lowering. All three positive projects fail with unsolved goals. The issue's project leaves exactly the goals of the issue.
2. reduceCtorEq removed. All three positive projects fail on their disjointness case.
3. Every injEq lemma removed. The issue's project and the two-field project fail. The Option project needs only disjointness and still verifies.
4. false_implies removed. The two-field project fails with ⊢ False → 0 = p.
5. The false statement made true. The case fails at its expectation that verification fails.

Not exercised: Except.error.injEq, Except.ok.injEq and List.cons.injEq. No project equates two Result or two List constructors, so removing one of these alone leaves the case green. The record says so.

Identity

No compiler-semantics identity moves. The IDs are digests of language/ and schemas/, and this change touches neither. No lock or expected record is regenerated. The other committed uses of term_cases were rerun with the new lowering:

• the eleven RuntimeKeys* modules of compiler/
• RuntimeSupport and RustRuntime, also under language/rust-runtime-1.2/

cargo xtask verify-examples reports that the normalized records equal expected/verify for:

• compiler, stdlib, std-models, std-reasoning and bootstrap, on the merged head
• every example except uor-atlas, on 1282b38 before the merge

Run locally (WSL, Linux x86-64, Lean 4.32.1)

• conformance_sm_35, _sm_36, _sp_25, _rb_16, _rb_17, _rp_07 and _rp_11 pass.
• validate-model, validate-spec-links, check-test-inventory, cargo fmt --check, clippy on lexlean and repo-conformance with -D warnings, cargo test -p lexlean --lib, and the bdd meta-gate pass.

Not verified locally

• uor-atlas. CI's Atlas shards are the evidence.
• conformance_sp_22, the runtime refinements. The kernel's OOM killer stopped it inside a 10 GB memory scope both with this lowering and on the unchanged release/v0.4 head f057b83. The limit is the host, not this change, and CI's bdd-preservation-runtime job is the evidence.
• The rest of just vv.

🤖 Generated with Claude Code

[humuhumu33]

Merged release/v0.4 (936eb3d) into this branch: merge commit bfb9409, no conflicts (CHANGELOG.md and VERIFICATION.md needed nothing), SM-35 amendment untouched. Branch is MERGEABLE, ci is re-running on the new head. Still a draft.

RP-14: the failing assertion (repository.rs:344, a push of a merge whose tree equals its verified second parent expected to plan nothing, got the whole gate) reads only .github/ci-plan.sh, .github/vv-rows.json and ci.yml. This PR touches none of them, and none changed on the base since 902d7de. I did not find a cause on the branch and could not reproduce the failure: after the merge, locally on Linux (WSL, pinned toolchain), conformance_rp_14, conformance_sm_35, conformance_sm_36 and cargo xtask validate-model all pass. I did not get a pre-merge run of RP-14 for comparison. If just vv (rest) fails on RP-14 again, the cause is in the runner environment or the test, not in this change.

Not run locally: SP-22 and the Atlas (CI carries both).

[afflom]

Maintainer review of bfb940922 (read from the diff, nothing built). The change is small and well made, and it is a widening of SM-35, not a defect fix: the old statement described the old lowering exactly (simp only over the named definitions, the hypothesis and a decided conditional), the theorem of #280 was rejected as specified, and the register was true. The PR amends the statement to a new positive claim (refutation of an equation between different constructors, the injectivity equation of every constructor with a field of Option, Result, List and each declared inductive, the fixed closing rules). #280 carries no milestone, and the owner has ruled that v0.4's scope is the milestone as written, so this does not land on release/v0.4.

What checked out, for the record: the rule set stays fixed and closed (every rule written in the script, reduceCtorEq a built-in simproc, the rest core lemmas); no sorry, admit or native_decide, the policy exact with [propext]; constructor names go through member and identifier; conformance_sm_35 asserts the generated rule list for five projects, Lean-backed, with refusal via LLV7002; five plants with red lines; statement byte-equal across the row, §31, the scenario and CONFORMANCE; R4 and R5 clean; no identity-bound file touched, though a lowering change is exactly what proof_lowering in language/semantics-1.2.toml versions (§21.2), and whether it bumps is a question to settle when it lands.

Where it goes: release/v0.5, which does not yet carry term_cases because the line has had no forward merge since 998927881. I owe that forward merge after the #91 heap half lands; when it is in, retarget this PR to release/v0.5, merge the line, settle the proof_lowering question, and I land it there. If the owner adds #280 to the v0.4 milestone, say so here and the order changes.

---

Generated by Claude Code

[humuhumu33]

Merged release/v0.4 (b06423e, with #262) into this branch again: merge commit 26b1493. One conflict, CHANGELOG.md, resolved by keeping both entries, the line's first (the RP-18 crates.io entry, then this PR's term_cases entry). VERIFICATION.md merged cleanly. No projection needed regenerating, and the SM-35 amendment is untouched: the branch differs from the base only in SM-35 and term_cases.

Branch is MERGEABLE and ci is re-running on the new head. The previous head (bfb9409) was green, just vv (rest) included. Locally on this merge (Linux, WSL): conformance_rp_14, conformance_sm_35, conformance_sm_36 and cargo xtask validate-model pass. Not run locally: SP-22 and the Atlas (CI carries both). Still a draft.

[afflom]

release/v0.5 now carries the 0.4.0 line (#322 merged at 61b4638cd; register 472; #279's loop-end row is RB-22 and #126 stage 2's rows are SL-06 to SL-08, the release/v0.4 rows keeping their numbers). Merge origin/release/v0.5 into this branch and recount; it then proceeds in the v0.5 order. The second forward merge (H5, H6, the release-workflow fixes) follows #304's landing.

---

Generated by Claude Code

[afflom]

release/v0.5 moved: the second forward merge (#327) is merged at 1046646ed, bringing release/v0.4 at a1b925dc6 (the v0.4.0 tag, H5 #298, H6 #304, the release-workflow fixes #320/#321/#323) onto this line. Language 1.2 identity dcdf8a721708f0a9c5e57303f78eef5f5e37c58b7a11a04272d8670f618a699f (1.1 and 1.0 unchanged); register 474 (RB-21 and SP-30 join; RB-16, RB-17, RB-19, RB-20, SP-29, BS-05, BS-06, BS-09 restated). Before the next push here, merge origin/release/v0.5 by merge commit and recount; locks and records are regenerated at the landing, not in the draft.

---

Generated by Claude Code