[afflom]

SM-37: nested_induction, induction over a nested inductive type through its recursor (#278). Draft; stacked on DF-19 (#284, branch claude/issue-278-df19-family, head 9d0896b18, with the maintainer's review fix), so the diff here is SM-37 alone. Review DF-19 first. Waits for the maintainer's acceptance of the design at #278 (comment) (accepted at #278 (comment), with the two conditions below). Based on release/v0.4 through #284; release/v0.4 is not merged into this branch.

History is the R3 order: commit 1 (904c1afc0) is the row, the SPEC §31 row, the scenario, the failing named test conformance_sm_37 and the induction-nested-type negative fixture with the new message; commit 2 (1ee15eff6) is the implementation; commit 3 (0b0c95d96) is the maintainer's review round.

What

A language-1.2 theorem about a value of a nested inductive type (one that holds itself under List, Option, Result or a product, in no mutual group) may be proved by nested_induction: the proof names a parameter of the theorem, states one proposition for each auxiliary member of the type's recursive family (DF-19's family_members) in the order of Lean 4.32.1's recursor, and gives a branch for every constructor of the type and of each member, binding the fields then one hypothesis per field that is a family member.

• Linker (ir/semantic.rs): check_nested_induction refuses, as LLT4001 before any backend, a use in language 1.1, a scrutinee that is not a theorem parameter of a nested document inductive in no mutual group, members missing / repeated / outside the family / out of order, a binder shared by two members, a proposition that is not a Prop, and on every level a missing or repeated branch, a branch for no constructor, and a wrong binder count.
• Backend (backend/semantic.rs): lowers to induction x using T.rec (motive_2 := fun b => P) … and one positional next binders => per minor premise, in the recursor's order whatever order the branches are written in (widen.rs sorts them). Goals are positional because nil/cons of two members share names, which induction … with refuses. The scrutinee must be a theorem parameter so the backend knows its type to name T.rec (Environment.proof_parameters).
• induction keeps refusing a nested type; its message now names nested_induction. DF-13's case still asserts the refusal.
• Both schemas gain the step; SPEC §16.9, §17.10 and §17.12 rule 7, CHANGELOG and a VERIFICATION.md record are updated.
• examples/nested-induction: leaves_le_size over Json (four motives, nine goals) proved by nested_induction, with mutual size/leaves groups over the family (DF-19).

Inherits the DF-19 review fix

The family is DF-19's family_members, so the fix to mentions_family_group (a group counts only at its own type arguments, #284) reaches SM-37's motive count. conformance_sm_37 now has a Rose (Rose Nat) case: rose = rose proved by nested_induction with the one member List (Rose (Rose Nat)), lowered to induction rose using Rose.rec (motive_2 := ...) with no motive_3, verified under the pinned Lean, plus a plant naming List (Rose Nat) as a member (refused). With the arguments ignored again the case fails (nested_induction is missing the member Rose (Nat) of the recursive family of Rose (Rose (Nat)), VERIFICATION.md). The plants are 49 now. The fallback of the same function in family_constructors is dropped, as in DF-19.

Maintainer's conditions

1. Motive and binder order are Lean 4.32.1's; the case plants a reordered member, a wrong binder count and a missing branch on each level. conformance_sm_37 does: members swapped (3 pairs), a binder too many and too few and a missing branch for every branch of each of the four levels (Json, List Json, List (String * Json), String * Json), and every level written in reverse lowers to the same Lean. 49 plants, all LLT4001, no backend output written.
2. The axiom set is the one the real build observes. The first verify of the example with an empty policy failed with LLV7005 … observed [Quot.sound, propext]; the example's policy and the SM-37 row now state propext and Quot.sound (ids.toml, SPEC §31, the scenario, CONFORMANCE.md regenerated and validate-model current). Not the prototype's set by assumption: it is the observed one, and they happen to agree.

Bumps (declared)

language/semantics-1.2.toml: semantic_ir 15 → 16, proof_lowering 3 → 4. Both schemas (semantic-module-v2, semantic-snapshot-v2) change. This moves the §21.2 identity, so SM-37 takes the identity slot (after #255, #259, #262, #264, #265; before #92 bootstrap landings). Nothing else the digest binds is regenerated here.

Measured (this host: 2 cores, debug build, Lean 4.32.1, rustc 1.97.0, under the shared heavy-job lock)

• Example under the pinned Lean: lexlean fmt (canonical), lock --check (current), check, build, verify: verified 1 module; attestation c7af737dad4c8d13d8835083917ceeaadf066a1b5a1fb623e544c374ec2ac573, 19.3 s. The generated Lean is induction value using Json.rec with motive_2/3/4 and nine next goals (next =>, next content =>, next items itemsHypothesis =>, next entries entriesHypothesis =>, next =>, next head tail headHypothesis tailHypothesis =>, ×2, next key content contentHypothesis =>).
• conformance_sm_37: passed, 41.0 s (verifies the example and a parameterised Rose under the pinned Lean, then the 49 plants, the language-1.1 use, and four scrutinee misuses).
• conformance_df_13, conformance_df_19: passed (with the stale locks of examples/recursive-data and tests/nested-family regenerated locally, not committed).
• cargo test -p lexlean --lib: 213 passed, 21.0 s. cargo fmt --all --check, cargo clippy --workspace --all-targets --all-features -- -D warnings (1 m 00 s), cargo xtask validate-model (447 ids), validate-spec-links (447 rows), check-test-inventory (779 tests: 287 + 492): clean.
• conformance_ex_07 on a tree with every fixture lock regenerated locally (not committed): 1170 s; the new induction-nested-type message matches; it fails only on certificate-{b,e,heartbeat,}-rejected, certificate-resource-exhausted and production-expectation-stale (their expected/command.json bind the identity) and on the two lock-schema-language-mismatch* fixtures, whose deliberately wrong locks my local blanket relock overwrote.
• Plant (VERIFICATION.md): comparing the members as a set instead of the recursor's sequence makes conformance_sm_37 fail (check fails, the swapped-members plant is accepted).
• Not run: just vv, the full workspace test, the host matrix (CI runs them; this draft runs only the rest leg).

Review round (head 0b0c95d96)

Maintainer's review at #292 (comment), answered point by point on this PR.

• examples/nested-induction/lexlean.lock is dropped; conformance_sm_37 locks its own copy of the example.
• backend/semantic.rs: proof and proof_branch return Result, and a nested_induction scrutinee with no named parameter is an LLI9001 diagnostic, not a guessed <local>.rec.
• conformance_sm_37: Lean-backed positive cases with a member under Option (none, some) and under Result (error, ok), goals asserted in the recursor's order; with the Option rows swapped the case fails (VERIFICATION.md). The language-1.1 use and the four scrutinee misuses go through refuse_project (LLT4001, the message, no backend output).
• The SM-37 row, §31 and the scenario say "names a parameter of the theorem"; CONFORMANCE.md regenerated (validate-model current).
• Lib-test count: 213 in VERIFICATION.md and here.
• Re-run on 0b0c95d96, under the lock: conformance_sm_37 passed (77.1 s), cargo test -p lexlean --lib 213 passed, conformance_df_13/df_19 passed (fixture locks regenerated locally, not committed), fmt and workspace clippy -D warnings clean, validate-model, validate-spec-links, check-test-inventory pass.

Landing list (the maintainer's regeneration at landing)

1. The register count: the branch carries 447 and is left as is. With #91 stage 4, H1: RuntimeSyntax grows by the heap constructs — the probe module (RB-19) #255 (448) and DF-19 (449) ahead of it the merged size is 450. The merge conflicts on exactly the count sites: README.md:150, the SPEC §31 total, crates/conformance/src/cases/repository.rs:763, xtask/src/spec_links.rs:64-65, and the "The register is 447 IDs." sentence of the CHANGELOG.md entry (it auto-merges and goes stale silently).
2. Every lock under the new identity: all tests/** fixture locks, examples/*, compiler, stdlib, packages and bootstrap. They are stale on this branch (LLC0102 … the compiler semantics changed since locking), so every test that opens one fails here until then. Nothing is regenerated here: examples/nested-induction carries no lock (the case locks its own copy), so EX-08 stays red for it until landing. The induction-nested-type fixture lock records the base ID.
3. Goldens and records the digest binds: tests/negative/certificate-*-rejected/expected/command.json (5), production-expectation-stale/expected/command.json, bootstrap/expected, the production packages and stack bounds, the normalized verification records; and examples/nested-induction/expected/{build,verify} (new example, not generated here: cargo xtask verify-examples --write has no single-example mode and would rewrite every other example's records).
4. examples/nested-induction retitle follows Seven examples carry the literal example's \title{Natural number addition} #251 (README notes it).

https://claude.ai/code/session_01F4DJnZorC2Jd4MJfN9DbZk

---

Generated by Claude Code

[afflom]

Maintainer review of 1ee15eff6 on 9d0896b18 (read from the diff, nothing built): accepted, one small round before the landing; nothing blocking.

The lowering is the agreed design (#278, comment 6346669084): induction x using T.rec (motive_k := fun b => P) with positional next goals (backend/semantic.rs:1315-1355), motive index index + 2 over members whose order the linker forces to equal the family as a sequence; branches sorted into minor-premise order by widen.rs::nested_branches after the check and before render, so written order is irrelevant and the case proves it. nested_family calls the argument-aware family_members of 9d0896b18; nested_branch_types gives the fields then one Prop per field in the family, in field order, which is Lean's rule; Rose (Rose Nat) gets two motives and label : Rose Nat no hypothesis, as the case asserts. Axioms observed [Quot.sound, propext], verified under the pinned Lean by verify_ok_backed with lean_backed asserted on the normative host; no sorry, admit or native_decide; emitted names are identifier()/self.member() rendered (R7, R8). R5: all refusals LLT4001, no unwrap or index on user data. R3: row, §31, byte-equal scenario, conformance_sm_37, fixture, plants that fire. Schemas additive. R4 clean. Downstream: nested through List (Json.array, Rose) and List (String * Json) (object) covered and verified; mutual groups and generalizing out by stated design.

Should fix

1. examples/nested-induction/lexlean.lock:3 pins compiler_semantics = 81a5f530…, a moved ID, while every other lock pins the base 30c5829b…. Drop that lock from the PR (or leave it pinned at the base ID); every lock, record and expected tree regenerates at my landing on the identity that is current then. examples/nested-induction/expected/ is absent, so EX-08 is red on this branch until then; the body says so, good.
2. backend/semantic.rs ~1327: owners.get(scrutinee).map_or_else(|| format!("{}.rec", identifier(scrutinee)), …) emits <local>.rec for a scrutinee that is not a named parameter. Unreachable after the linker's proof_parameters check, but a guess rather than a refusal: thread the backend's internal(...) diagnostic as render_module does.
3. Coverage: nested.rs exercises List and product members only; the none,some and error,ok rows of family_constructors are asserted by no Lean-backed nested_induction case. Add one positive member of each so the minor-premise order claim is armed.

Nits: the SM-37 row, §31 and scenario say "the proof names the local" while the implementation and §17.10 require a theorem parameter and refuse a non-parameter local; say "names a parameter of the theorem" and regenerate CONFORMANCE.md. In nested.rs, the language-1.1 case and the four scrutinee misuses assert by message only; route them through refuse so the "all 49 are LLT4001 with no backend output" claim is checked. VERIFICATION says 212 lib tests, the body 213.

Landing: SM-37 moves semantic_ir 15→16 and proof_lowering 3→4 in language/semantics-1.2.toml, so the compiler-semantics ID moves; it lands as its own identity wave after the #91 heap half, stacked on DF-19 (#284, accepted at 9d0896b18). The digest-bound records, locks and expected trees are mine at that landing; retarget to release/v0.4 happens then.

---

Generated by Claude Code

[afflom]

Thanks. Everything is done and pushed to claude/issue-278-sm37 as 0b0c95d96, still stacked on DF-19 at 9d0896b18 (that branch is untouched).

Should fix

1. The lock. examples/nested-induction/lexlean.lock is removed from the PR. The example carries no lock; conformance_sm_37 locks its own copy of it (example_copy), so the case does not depend on a committed lock. EX-08 stays red for this example until your landing, and the body says so.
2. The <local>.rec fallback. proof and proof_branch in backend/semantic.rs now return Result<String, Diagnostic>, and a nested_induction scrutinee with no named parameter is an LLI9001 diagnostic (phase lean-backend: ...), as render_module does. The one caller (the theorem renderer) propagates it.
3. Option and Result coverage. Two Lean-backed positive cases in conformance_sm_37: Chain | link : Option Chain -> Chain and Attempt | wrap : Result Attempt Nat -> Attempt, each with one member and a reflexivity proof, verified under the pinned Lean. They assert the goals in the recursor's order (next rest restHypothesis =>, next =>, next value valueHypothesis =>; and next outcome outcomeHypothesis =>, next code =>, next value valueHypothesis =>), exactly two motives, and the branches are written in the opposite order of the minor premises. Arming check: with the Option rows swapped in family_constructors (some before none) the case fails at the Option assertion; recorded in VERIFICATION.md, plant restored.

Nits

• The SM-37 row (ids.toml), SPEC §31 and the scenario say "the proof names a parameter of the theorem"; CONFORMANCE.md regenerated with cargo xtask validate-model --write (SM-36's row, which does say "the local", is left alone).
• The language-1.1 use, the four scrutinee misuses and the member-of-another-instantiation plant now go through refuse_project, which asserts LLT4001, the message, and that build writes no output.
• Lib-test count: 213 in VERIFICATION.md and in the body.

Re-run on 0b0c95d96, under the heavy lock: conformance_sm_37 passed (77.1 s); cargo test -p lexlean --lib 213 passed; conformance_df_13 and conformance_df_19 passed (with the two stale fixture locks regenerated locally, not committed); cargo fmt --all --check and cargo clippy --workspace --all-targets --all-features -- -D warnings clean; validate-model, validate-spec-links and check-test-inventory pass. Counts untouched (447 on this branch; 450 merged, sites listed in the body).

🤖 Generated with Claude Code

https://claude.ai/code/session_01F4DJnZorC2Jd4MJfN9DbZk

---

Generated by Claude Code

[afflom]

Maintainer: the round at 0b0c95d96 is accepted. The example's lock is gone and conformance_sm_37 locks its own copy (nested.rs:35-39); proof/proof_branch return Result and a scrutinee that is no theorem parameter is LLI9001 (backend/semantic.rs:1331-1341, registered), the .rec site is one; OPTION_CHAIN and RESULT_ATTEMPT are Lean-backed with the goal order, the recursor and exactly motive_2 asserted; the statement says "names a parameter of the theorem" byte-equal across the row, the scenario and §31; the language-1.1 case and the four misuses go through refuse_project with LLT4001 and no backend output. Eight files changed since the last head, nothing identity-bound beyond the two record bumps.

SM-37 lands as its own identity wave after the #91 heap half, stacked on DF-19 (#284); I retarget, regenerate and recount then.

---

Generated by Claude Code