One Integer for Semantic Work and Materialization: A Mechanized, Content-Addressed Combinator Machine over Term, Budget and Content Environment, and the Engineering of Trustworthy Proof Artifacts

We present Σ-GLYPH Book I, a content-addressed combinator machine in which a single unsigned integer budget — ATP — prices both the semantic work an evaluation performs and the peak number of nodes it materializes, and we report a layered Lean 4 mechanization of it. Three framing statements come first, because an earlier version of this paper stated the first two wrongly in its summary and did not state the third at all. Evaluation is a relation over three inputs, not two. eval takes a term hash, a uint32 budget, and a content environment — a partial map from NodeHash to bytes whose entries hash to their own key. A demanded hash absent from that environment is a canonical outcome, so availability sits inside the semantics: a node holding the bytes reaches a normal form where a node without them returns Unresolved Reference, on the same term and the same budget. What bounds this is a monotonicity theorem, evalHash_stable: extending an environment can change only an unresolved outcome, never a normal form and never an exhaustion. The bound is semantic, not physical. size counts materialized nodes. The theorem says nothing about resident set size, heap bytes, evaluator stack, the store's index, hashing buffers or allocator behaviour; the correspondence between the two is a refinement layer we do not prove and do not claim. A result hash does not say how the run ended. eval returns a receipt — exit, result hash, ATP spent — and the hash alone never carried the exit: DISSONANCE(ATP Exhausted) is an ordinary term, so one digest is reachable both as an exhaustion and as a normal form. A consumer reading only the hash cannot tell "finished" from "ran out", and because the budget is also the licence over the verifier's memory, a verifier must be able to refuse a term before evaluating it — a refusal that is a deployment decision and not a canonical outcome. The central theorem, EvalMachine.evalHash_peak_size, is 𝑠𝑖𝑧𝑒≤𝑎𝑡𝑝+1size ≤ 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 𝑐𝑜𝑠𝑡−1cost - 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. Forty-one theorems across five fronts are guarded; all sixteen evaluator theorems have axiom cone {𝚙𝚛𝚘𝚙𝚎𝚡𝚝,𝙲𝚕𝚊𝚜𝚜𝚒𝚌𝚊𝚕.𝚌𝚑𝚘𝚒𝚌𝚎,𝚀𝚞𝚘𝚝.𝚜𝚘𝚞𝚗𝚍}\{propext, Classical.choice, 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; three further bridges check a weaker correspondence — 861 oracle steps against the premise the proof consumes, 3000 random closed λλ-terms against a transcription of the Lean compiler model, and 1220 store perturbations against the monotonicity bound; and a three-engine randomized fuzzer generates 5347 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]. Version note. This is version 2 (label 0.7.0-paper2) of the paper first deposited as 10.5281/zenodo.22069651 (label 0.6.7-paper1). It corrects the v1 summary — the evaluator is a relation over term, budget and content environment, and the proven bound is semantic (materialized nodes), not physical — adds the receipt/admission framing (§3.6–§3.9) and the correction record (§7), and re-measures §6 at the adopted v0.7.0 release. Source archive sigma-glyph-47cf57d.zip is git archive of commit 47cf57dd6ec2f671d5aaf521094420f97cf566d6. paper.pdf is reproducible byte-for-byte from that commit with SOURCE_DATE_EPOCH=1788134400, pandoc 3.10.2 and tectonic 0.17.0; its SHA-256 is 8970a3af97c5e497361a80560e8804c386ec52eb18cf687b22e3a8905ccf9565. Deposited is not reviewed: a DOI is a permanent address and a frozen artifact, not a venue or a peer review.