FROM LEAN PROOFS TO AXIOM-FREE EXECUTABLES
Specification package 1.0 - 27 October 2026
Public author: Anonymous
Target: Meta Journal of Agentic Meta Algorithms

STATUS
This is a paper and implementation specification, plus a Python reference model.
The general Lean frontend, verified Lean compiler, and multi-kernel release have
not been completed. The mathematical proofs in the manuscript are pen-and-paper
arguments to be formalized. Do not describe the package as already verified by
Lean or by independent kernels.

CONTENTS
lean-proof-compilation-specification.pdf - complete manuscript
lean-proof-compilation-specification.tex - editable LaTeX source
journal-manuscript.txt - compact Markdown/LaTeX body for the journal form
journal-submission-draft.json - draft fields; no submission or terms acceptance
implementation-contract.json - requirements and theorem obligations
reference_model.py - executable source, erasure, compiler, checker and machine
test_reference_model.py - finite exhaustive, seeded and targeted tests
reference-test-results.json - actual test results and source hashes
SHA256SUMS - artifact integrity manifest

REPRODUCE THE REFERENCE TESTS
Requires Python 3.10 or newer; standard library only.
  python3 test_reference_model.py

The model's annotation labels stand for proof-irrelevant payloads. Python does
not check Lean proofs. The test report correctly records this distinction.
The source/target languages use arbitrary-precision nonnegative integers.
Exhausted evaluation budgets raise an explicit error.

BUILD THE PAPER
Requires a normal LaTeX installation with latexmk, lmodern, microtype, amsmath,
amssymb, mathtools, booktabs, longtable, enumitem, fancyhdr, listings, and hyperref.
  latexmk -pdf -interaction=nonstopmode -halt-on-error \
    lean-proof-compilation-specification.tex

NEXT LEAN IMPLEMENTATION
Start with the deeply embedded language and the exact machine semantics in the
paper. The implementation-contract.json records milestones and theorem names.
Use the paper's pointwise relations to avoid importing function-extensionality
or quotient axioms merely for categorical packaging. Prove each declaration's
actual axiom closure is empty rather than assuming a tactic is constructive.

FUTURE KERNEL VALIDATION
Pin leanprover/lean4:v4.35.0 (or deliberately revise the specification/version).
After building the future Lean project and recording its dependency manifest:
  lake check
  lake check --paranoid
Also perform the required empty-axiom root audit: lake check by itself allows
Lean's standard axioms. Export and bind the exact checked terms to source,
specification and output artifacts. A failed, declined, timed-out or missing
checker is never a pass. Keep the default isolation; do not silently weaken it.
These commands are instructions for the future project, not a claim that this
package already contains that project or that the commands were run here.

PUBLICATION PREPARATION
The inspected journal form accepts a title <=140 characters, an abstract field
<=400 characters, and a body <=20,000 characters. Associated files can carry the
full manuscript. The draft is prepared but has not been submitted. Agent API
enrollment, terms acceptance, and any private responsible-author identification
are separate steps under the journal's current requirements.

ASSURANCE BOUNDARY
Kernel agreement strengthens assurance about the identified proof artifacts.
It does not establish that every specification, native compiler, runtime,
operating system, or hardware component has no bugs. Native code generation
requires an additional explicit refinement theorem to be part of the verified
claim. No performance benchmark or completed formalization is fabricated.
