feat(preservation): certificate A as kernel-term data (stage 3 of #89)

[afflom]

Refs #89

Draft: stage 3 of #89, certificate A as native core-module data on the vehicle of #146 (production/kernel.rs). Built on claude/issue-89-typed-certificates; to be merged with main when #146 lands.

Register

SP-15 (R3 order: register row, SPEC §31 row, scenario, failing named test conformance_sp_15).

Done so far (measured, pinned Lean 4.32.1, Linux x86-64)

The data generator production/certificate/data_a* builds certificate A without any Lean text. Roots whose data certificate A was compiled, replayed with leanchecker, and passed the exact axiom audit by the dev harness (cargo test -p repo-conformance --lib dev_certificate_a -- --ignored):

• production: R0, R1, R2, R4, R5 (5 of 6; R3 is well-founded recursion)
• production-coverage: R9, R10, R11, R12, R13, R14, R15, R16, R17, R18, R19, R20, R21–R29, R30, R31

Library growth so far: zero declarations (every implicit binder of the lemmas used is a part of what the generator holds, or is fixed by the type of an argument).

Remaining (tracked in the PR as it goes)

well-founded recursion (3 certificates), collection templates, boundary validators and entry, conformance cases that read the A text, the statement oracle record, planted defects, regeneration of records.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WG9wejRSGKo2jLG8BLxPs5

---

Generated by Claude Code

[humuhumu33]

Content review of #157 at 7653ed1 (train member; formal approval goes on the final #167 head). Re-checked on #167 at cde36cd, which removes A's ignored developer tests (the RP-08/RP-12 failures); the items below still stand there.

What holds: certificate A's text generator is gone from production/certificate.rs (the remaining render_* serve certificate B and the differential evaluator), the preservation library did not grow (no file under language/ changes), the register count is 403 in all four places, and A-STATEMENTS.md compares all 1326 rows by Kernel.isDefEq.

Blocking:

1. No VERIFICATION.md record for SP-15's plants, on this head or on #167. conformance_sp_15 runs five plants (cases/preservation.rs:4005-4164); record their red output in the form of the SP-14 section (VERIFICATION.md:1364).
2. Certificate A is built whole, rendered to Lean text and to notation, and only then checked against max_file_bytes (certificate.rs:543-554). The text generator checked part by part (ea0a4ed certificate.rs:2754, 3378, 3389, 5690). SPEC.md:4817-4824 still promises that each term, arm, encoder, function and the boundary are counted as built. Either restore an incremental budget in the Writer (before lean_text_legacy), or rewrite that paragraph with what now bounds A's generation.
3. 7653ed1 counts any error prefixed "phase preservation:" as a caught lowering plant (preservation.rs:1969, cases/preservation.rs:89-101). That prefix is every LLI9001 the generator raises, so a generator bug counts as "caught", the locus is not checked, and no plant has to reach the kernel. SP-02's row says each rejection lies in the mutated function's declaration. Make the refusal name the function and site and assert it, require one kernel rejection per mutation kind, record the counts, or amend SP-02 with the soundness argument.
4. SP-02's row still says a match on 420 constructors is not refused (SPEC.md:9494, model/ids.toml:1845, CONFORMANCE.md:353, preservation.feature:13), but the default limit now accepts about 240 (stress.rs:1259; SPEC.md:4927-4929), because A is weighed by its notation. That narrows language-1.2 acceptance; state it in CHANGELOG and fix the row and SPEC.md:4924-4925 ("so does one on 300").

Should-fix:
5. COSTS_A is fitted with a 5% margin (lower.rs:517-534) and on random_shapes(24, 0x5eed) (preservation.rs:3467), the same set SP-02 calls held out (cases/preservation.rs:433). lower.rs:489 and SPEC.md:4787/4795 still say "half" and "none fitted" (also on #167). 00f3a30 shows the margin is thin. Refit without the held-out seed or use a fresh one, and state the margin.
6. The oracle maps the data's own constants to the text's before comparing (preservation.rs:3163, swapRoot), so the 43 definitions whose bodies differ (A-STATEMENTS.md:44) are not shown equal. That is harmless for width predicates (the root's "exactly" fixes them), not for an encoder or denote. List the 43 rows and give evidence for any that is not a width predicate.
7. The VERIFICATION.md SP-02 cost plants are stale: type node "272 to 2000" (cost now 0, :1556), arm pair "180 to 500" (cost now 1018, :1566-1572, output from the old run). Re-plant and re-record.
8. SPEC.md:4829-4832 (and #167 :4950-4955) still says types are not shared and the generic chain is refused from 14; false for A as data.
9. The production compiler reads LEXLEAN_SHOW, LEXLEAN_SHOW_FILE and LEXLEAN_AXDBG (data_a.rs:366, 383-389), and LEXLEAN_SHOW_FILE writes a file to a path the environment picks. SPEC §23.1 says four operational variables exist and change no output. Please remove the hooks (they survive on cde36cd).

Nits: two sizes of A read by different rules (notation for max_file_bytes, Lean text for the quarter rule, verify/mod.rs:967 vs 2394); SP-15 plants check only "error" and the changed-statement plant renames Bool.true module-wide (cases/preservation.rs:4016, 4030); the SP-15 scan is 8 phrases (:3893, superseded by SP-17); empty impl blocks (certificate.rs:1097, 1426, 2971); the PR body is stale (remaining work is done, 5/6 roots is now 57/57).

This is a comment review; formal approval will be given on the final #167 head once 1-4 are fixed there.