[v0.4] #27 stage 2: preservation and certification proof libraries as native core modules #79

Child of #27; plan and rationale in this comment.

Scope

Remove the handwritten Lean libraries from the release tree. Their content becomes native core-module/1 LexLean source (SPEC §17.10), and the Lean the verifier compiles is generated from it by the compiler.

• language/preservation-1.2/library/LexLeanPreservation/*.lean (13 modules, 934 registered declarations);
• compiler/proofs/LexLeanCertification/*.lean (13 modules, 107 registered declarations).

Work

• A one-time lossless exporter, run by the pinned Lean over the elaborated environments, outside the release tree and recoverable from a commit (the Atlas precedent, examples/uor-atlas/MIGRATION.md).
• Extend the core-module schema, linking, and both backends only where the libraries need a construct it lacks (each extension registered under R3 with its own scenario and test).
• The libraries become language data of the embedded compiler project: native .lex.tex modules, with the library registry (declarations and their exact axioms) checked against the generated Lean's axiom audit.
• The verifier stages the Lean generated from the native modules, not a committed .lean file; certificates A, B, E and the production corpora elaborate against it unchanged.
• Re-point every gate that reads the library text (statement vocabulary, correspondence audit, SP-04, GC-09, shipped-module and registry checks) at the native source or its generated artifact.
• A permanent condition, in the manner of VR-19, that no independently authored Lean implementation of these libraries exists in the release tree.

DoD

• No handwritten Lean contains the preservation or certification libraries.
• The library source is ordinary closed .lex.tex that can be snapshotted like any project, content-addressed and reproducible.
• Every registered declaration, with its exact axioms, is unchanged, and generated modules import only Init and the generated graph.
• Editing generated Lean cannot become authoritative: regeneration restores it, and a planted source-versus-generated drift is caught.

Acceptance criteria

• Equivalence evidence: re-exporting the regenerated environments equals the original export declaration by declaration (types, values, reducibility, attributes), recorded in a migration record.
• Lean elaboration, leanchecker replay and the exact axiom audit pass for the generated libraries, and for the certificates of every production corpus built on them.
• Planted defects (a changed declaration, an added axiom, a stale generated module, a handwritten .lean file reintroduced) each turn a named gate red.
• Public compatibility: languages 1.0 and 1.1 are byte-identical; language 1.2 identities are regenerated and the change is recorded.
• Full just vv passes.