fix(model): MN-02 states what the shipped package does

[afflom]

Item M1 of the completion plan #3, closes #4.

The false claim. MN-02 said the root's runtime closure contains no recursion. The source has none, but the committed package renders each list fold as a function that calls itself. This is UOR-Foundation/LexLean#105, and docs/evidence/rendering.md already describes the fold drivers as recursive. 15 generated functions of dist/packages/rust-std/mnist/src/lib.rs call themselves.

The change.

• MN-02 (register, scenario, CONFORMANCE.md, and the README sentence that repeated it) now states what holds: exactly the allocation and overflow effects; no recursion in the source; a stack depth bounded by the list lengths the 784-byte precondition fixes.
• conformance_mn_02 keeps its eligibility checks and adds the fact: it finds the generated functions that call themselves and fails when there are none. That failure is the signal to restore the stronger claim once LexLean renders folds as loops (LexLean#105, item L0.1 of [0.5.0] Completion plan: optimal compilation for every production root LexLean#106).

Falsified. A package whose generated functions no longer call themselves makes the test fail with no generated function of the package calls itself: restore MN-02's claim of no recursion; the committed package restored passes. Recorded in docs/evidence/planted-defects.md.

Checked locally, with Rust 1.97.0 (1.97.1 was not downloadable in this session) and LexLean built at the pinned 54f2ec41: conformance_mn_01, _02, _03, _06 pass; cargo fmt --check, cargo clippy --workspace --all-targets -D warnings and xtask check-model pass. The acceptance jobs fail on main too (prismpm.lock is absent until #11); the model job is the gate this change must pass.

🤖 Generated with Claude Code

https://claude.ai/code/session_013Eo1UJoRXDrVSdkPw8UC35

---

Generated by Claude Code