One Integer for Work and Memory: A Mechanized, Content-Addressed Combinator Machine, and the Engineering of Trustworthy Proof Artifacts

Abstract

We present Σ-GLYPH Book I, a content-addressed combinator machine in which a single unsigned integer budget — *ATP* — prices both the work an evaluation performs and the *peak* memory it materializes, and we report a layered Lean 4 mechanization of it. The central theorem, `EvalMachine.evalHash_peak_size`, is $\mathit{size} \le \mathit{atp} + 1$ at **every** configuration the run passes through, proven *on a model of the actual hash-thunk evaluator* rather than on an abstract cost algebra: the per-step accounting lemma `size_step` establishes that every priced action grows the term by at most $\mathit{cost} - 1$, which is exactly the row-by-row correspondence an abstract proof has to assume. A companion theorem, `evalHash_settles`, shows that the machine's answer is a configuration on which no further action fires — so a run ends because the machine settled, not because a fuel counter cut it off, and every run exits through exactly one of normal form, ATP-exhausted or unresolved-reference. The mechanization is layered down to bytes — a from-scratch FIPS 180-4 SHA-256 in core Lean, serialization injectivity, round-trip canonicity and validation totality — so that redex recognition by hash is *derived* rather than re-axiomatized. Thirty-six theorems across five fronts are guarded; all eleven evaluator theorems have axiom cone $\{\texttt{propext}, \texttt{Classical.choice}, \texttt{Quot.sound}\}$ exactly, with `native_decide` confined to ten theorems in other fronts whose documented trusted base already names the compiler. We are equally explicit about what is *not* proven. The correspondence between the Lean model and the running implementations is empirical: three differential bridges execute the compiled Lean model against the reference oracle on 33 evaluation vectors, 334 byte buffers and 582 wave cases; two further bridges check a weaker correspondence (861 oracle steps against the premise the proof consumes, and 3000 random closed $\lambda$-terms against a transcription of the Lean compiler model); and a three-engine randomized fuzzer generates 5185 evaluation vectors per CI run. Our second contribution is methodological, and we state it here in one paragraph because it changes how much the first should be believed. The CI machinery that asserts "these theorems hold and rest on these axioms" — not the Lean kernel, the Python around it — was defeated twenty-one times over six internal hardening rounds and five external reviews: by `sorryAx`, by a string literal that blinded the comment stripper, by a `#print axioms` override installed *by the audited module*, by vacuous theorems, by definition gutting that leaves every pinned statement byte-identical, by an audit whose scope came from a config field nothing compiled from, and — six rounds in — by a file walk that was not recursive. Every bypass was reproduced against a green build; not one required a kernel bug. §5 gives three representative vectors and the thesis that unifies them (*a control whose scope is chosen by the thing it controls*); the full taxonomy is a companion paper [@paperB2026]. --- Artifact. This record contains the paper as PDF and a snapshot of the source repository at commit 7ecba6ab283c89111a76a3a1edeba57339b4443c, including the Lean 4 proofs, the three reference implementations, the specification texts, and the adversarial review ledger. Reproducing the claims. From the archive: cd proofs && lake env lean SizeBound.lean checks the central theorems; python3 proofs/bridge_check.py checks that the per-step premise holds on the reference evaluator; python3 tests/spec_conformance/run_reference.py runs the 49 conformance vectors. All three were green on the archived commit. Authorship. The Lean formalizations, the reference implementations and much of the prose were written by AI models under the author's direction; the per-model review ledger is preserved in reviews/. Every theorem is checked by the Lean 4 kernel, and the trusted-base caveats are stated in proofs/README.md. See the Acknowledgements section of the paper.