[afflom]

Draft SM-37 source delivery (#429): nested induction through the nested type’s recursor. #284’s DF-19 prerequisite is now accepted on release/v0.4 as 1a690b51; this PR now targets that release line directly. The existing implementation at 0b0c95d96 has retained maintainer source acceptance, while its identity-bound artifacts and final gate remain incomplete.

Source-only reconciliation with pending Host 943bba379a is independently reviewed locally: tree da17a069, 34 paths, 472 authoritative claims and 303 negative cases. It preserves the accepted 599-line SM-37 case/49 plants, strict schema union, current Host renderer/runtime pins, and only the intended semantic_ir=16 / proof_lowering=4 changes. It corrects the example title with a project-local closed glossary. This preparation is not published on this PR, has no generated artifacts or execution claim, and awaits the coordinated post-Host identity wave. The current head remains 0b0c95d96.

The design was accepted at #278 (comment) with the conditions retained below. Historical measurements below describe their original heads and local setup, not final combined-tree acceptance.

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. These accepted axes and schemas move the §21.2 identity. Preserve the final base’s renderer/runtime pins during reconciliation and regenerate only in the coordinated post-Host wave. The current historical branch’s other pin values are not the final publication inputs.

Historical measurements at the original implementation heads

Recorded host: 2 cores, debug build, Lean4.32.1, rustc1.97.0, under the shared heavy-job lock. These measurements do not establish acceptance of the new source preparation.

• 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.

Remaining landing work

1. Reconcile the accepted source with the actual final release/Host head. The current branch’s historical447 count and earlier predicted450 are not the current union; the reviewed local preparation has472 authoritative claims/303 negative cases. Recompute any later union, preserve strict predicates and use the official projection writer.
2. Regenerate affected valid locks with official writers at the final compiler identity. Preserve deliberately invalid/older-language negative locks, their defects, diagnostic codes and exits; do not repeat the historical blanket relock that overwrote wrong-language fixtures.
3. Produce identity-bound fixtures, exports/packages/stack bounds, goldens and normalized verification records, including the new nested-induction example. Keep only actual writer output, review provenance and changed observations, and retain historical failed attempts honestly.
4. Run the applicable SM-37/DF-13/DF-19 evidence and the complete final-head gate on the real integrated source/artifacts; compare tested/reviewed/actual merge trees. No stale-head rerun or second concurrent identity wave is requested.
5. Close scoped SM-37: nested induction through the nested type's recursor #429 only after accepted merge. Parent Language 1.2: induction and structural recursion over nested inductive types #278 stays open until its full intended DF-19 and SM-37 delivery is verified.

https://claude.ai/code/session_01F4DJnZorC2Jd4MJfN9DbZk

---

Generated by Claude Code

Closes #429 (SM-37 delivery slice). #278 remains open until both DF-19 and SM-37 are accepted.

[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

[afflom]

Maintainer queue refresh at unchanged 0b0c95d96: the final SM-37 source round remains accepted, including Option/Result coverage and the backend refusal. It remains stacked on DF-19 (#284), which must integrate first. Current draft CI 39916071276 has a failing rest leg; job 120289944059 stops before BDD at examples/collections' stale lock (LLC0102). The skipped full-gate jobs are expected for this draft; no unchanged-head retry is requested.

After DF-19, the maintainer retargets/updates and reviews this integration, coordinates its schema/semantic_ir/proof_lowering identity wave and all official lock/export/golden/normalized-verification writers (including the new nested-induction example), reconciles counts, and requires focused SM/DF evidence plus the complete final-head gate and merged-tree evidence. Keep draft until that preparation is complete. Scoped delivery is #429; #278 remains open until both DF-19 and SM-37 are accepted. No duplicate implementation or independent writer run is requested.

[afflom]

Maintainer source review refreshed at 0b0c95d. No new source blocker found; the earlier source acceptance remains. The live base branch now points to reviewed DF-19 head 9f3ca00, whose full CI is still running. The old 9d0896b value in PR metadata is the shared ancestor, not the current branch head.

A read-only three-way integration against that current DF-19 head has six textual conflicts: README, SPEC, the examples/repository conformance files, language/semantics-1.2.toml, and xtask spec_links. The linker/backend/widening source combines textually. The two-head union is 471 claims and 303 prescribed negatives; the silently merged CHANGELOG total also needs correction. These are preparation counts, to be recomputed against the eventual landing base.

The identity resolution must retain the current base's renderer/runtime pins while adding SM-37's semantic_ir 15→16 and proof_lowering 3→4 plus its schema changes. Selecting the old semantics file wholesale would restore stale pins. This remains a later coordinated identity wave: after #284 lands, update/retarget this existing PR, reconcile the source, use official affected writers and obtain final-head acceptance. No duplicate implementation, writer, or test run was started. #429 is the scoped delivery; #278 remains open until both recursion and induction work land.

[afflom]

The DF-19 prerequisite is now actually merged on release/v0.4 as1a690b51, after its complete passing gate. I refreshed the accepted source review and current head0b0c95d96: the SM-37 implementation remains the existing delivery; its historical stale-lock CI does not invalidate that source acceptance.

I am carrying forward the existing six-conflict source reconciliation on this PR, preserving the reviewed implementation and current base identities rather than taking its old semantics pins wholesale. The pending Host integration943b adds another claim and current renderer inputs, so combined counts must come from the actual union. This is source preparation only while Host’s final gate runs; no second identity/product wave or unchanged-head CI rerun is starting. Keep #429/#278 open. The final changed head still owes official artifacts, focused SM-37/DF-13/DF-19 evidence and full acceptance before merge.

[afflom]

The reviewed SM37 source at 0b0c95d is retained by ancestry and source in the combined #393 carrier at 3fe13b5, with accepted Host/DF19 and BS16. Official products, including the new nested example and LLT4001 negative, passed their producer/artifact reviews. The full exact-head hosted CI41889333456 and reproducibility41889261587 are running; all SM37 plants and unchanged obligations remain required. Keep this draft and #429/#278 open. After complete combined acceptance, this PR will be explicitly superseded before carrier merge; #429 closes only after actual landing/tree equality, and #278 needs a separate full-scope reassessment.

[afflom]

Superseded by the reviewed combined delivery in #393, final head 050e96579b83f2f71dda78e1bf6a87791278582a. Final CI 41923290770 passed all 45 jobs, including honesty, required hosts, complete normative cases/plants and Atlas; reproducibility also passed. Final maintainer evidence review confirms the reviewed/tested tree 3065516167862533e0594427c28be8fe74406aae and retained original contributor ancestry.

I am explicitly closing this draft as superseded BEFORE the carrier merge. This is not a separate landing or an assertion that the old draft passed a complete gate. Its implementation, review corrections and history are retained by the carrier. Scoped issues remain open until #393 actually lands and its merged tree is verified; broader unfinished work is not closed by this supersession.