[afflom]

What it does

PR 0 of the plan on #278 (design: #278 (comment)): the R3 skeleton for the two capabilities the design names. It commits to nothing irreversible and implements nothing.

• Register rows SM-37 (nested_induction, an induction over a nested inductive type that lowers to the recursor the pinned Lean generates, with the auxiliary motives stated in the proof) and DF-19 (mutual definition groups recurse over the whole recursive family of a nested type), their SPEC.md §31 rows, CONFORMANCE.md (generated), and the scenarios in features/suites/semantic-ir.feature and declarations.feature.
• The failing named tests conformance_sm_37 and conformance_df_19: both fail on this head by design (no semantic-ir case is wired for SM-37, no declarations case is wired for DF-19).
• One negative fixture, tests/negative/induction-nested-type (prescribed in EX-07, 297 to 298): a type Json with array (List Json), mutual size/leaves groups the compiler accepts today, and leaves_le_size proved by plain induction, which is refused as LLT4001 ("requires a self-recursive inductive without nested or mutual occurrences"). It is the theorem that cannot be stated yet. It stays valid after the implementation, which keeps induction refusing nested types (only the message changes, to name nested_induction); its expectation is then rewritten by fixtures-write.
• The register moves 443 to 445 on this base; the maintainer assigns the final count at each landing (not renumbered here). The count is changed in README.md, crates/conformance/src/cases/repository.rs and xtask/src/spec_links.rs, as #91 stage 4, PR 0: register rows SP-21 and RB-15 (R3 skeleton) #223 did.

Not in this PR

• No implementation (PR 1: DF-19, stacked on this branch, no file of the §21.2 digest; PR 2: SM-37, the identity PR, stacked on PR 1). Those wait for the maintainer's answer on Language 1.2: induction and structural recursion over nested inductive types #278.
• No identity-bound record is touched. The fixture's lexlean.lock was made by lexlean built from release/v0.4 at 979606797 (this PR's base) and is current for it.

Gates (exact, run on this head)

cargo xtask validate-model         validate-model: documents current, 445 ids, 86 codes, meta-gate and audits clean (R1)
cargo xtask validate-spec-links    validate-spec-links: 445 table rows bijective with the register (RP-07)
cargo xtask check-test-inventory   775 tests; each in one part of .github/bdd-parts.json (RP-13)
cargo fmt --all --check            clean
cargo test -p repo-conformance --test bdd                     5 passed (R3 scenario/register equality, honesty meta-gate)
cargo test -p repo-conformance --test conformance conformance_rp_01 conformance_rp_07 conformance_ex_07
                                   3 passed (EX-07: all 298 fixtures, incl. induction-nested-type with LLT4001)
cargo test -p repo-conformance --test conformance conformance_sm_37 conformance_df_19
                                   2 FAILED by design (R3)

Planted defects (not committed):

• One word changed in the DF-19 row of SPEC.md §31: validate-spec-links refuses it (table and register statements printed side by side).
• One word changed in the DF-19 scenario title: every_id_has_a_scenario_and_a_test fails with R3: DF-19's scenario statement differs from the register (§27.7).

What CI runs

The full just vv does not run on the machine this was prepared on (2 cores, 7 GB); I ran the recipes above and leave the rest to CI. Because this PR adds a register row, a scenario and a fixture and implements nothing, I expect the rest part to be red only on conformance_sm_37 and conformance_df_19, as for #223.

---

---

Generated by Claude Code

[afflom]

Superseded by the two-draft restructure the maintainer asked for on #278: the R3 skeleton is not its own PR.

1. DF-19, DF-19: structural recursion over the recursive family of a nested inductive type (#278, draft) #284 (base release/v0.4): skeleton commits (row, scenario, named test), then the implementation. Identity-neutral; lands first.
2. SM-37, SM-37: nested_induction, induction over a nested inductive type through its recursor (#278) #292 (stacked on DF-19: structural recursion over the recursive family of a nested inductive type (#278, draft) #284): skeleton commits (row, scenario, named test, the induction-nested-type negative fixture), then the implementation with the version bumps (semantic_ir 16, proof_lowering 4), the example examples/nested-induction, the plants and the observed axiom set.

Closing this one.

🤖 Generated with Claude Code

https://claude.ai/code/session_01F4DJnZorC2Jd4MJfN9DbZk

---

Generated by Claude Code