Synthesis of the Information Universe: Relativity and Mass as Readouts of Retained Distinctions, Assembled from Classical Equations over a Machine-Checked Kernel

We synthesize an information-first account of relativity and mass from equations whose owners span Euler and Lagrange to Jacobson, anchored — joint by joint — on a machine-checked kernel of exact rational-arithmetic theorems (Coq 8.18.0, axiom-free at Tier 0; every Print Assumptions reported). The kernel establishes, as theorems: a double stationarity principle in which the field recurrence and the retention of graph edges are the two first-variation readouts of one quadratic action; an exact two-way balance between per-edge field strain and an affine function of Forman curvature; monotone laws of curvature and spectral data under retention; a per-edge frequency ceiling; the completeness of the lattice edge frame for symmetric two-tensors with an exact polarization key; an exact inside/outside/cut partition of the quadratic form of any graph against any region; and a Clausius-form restatement of the retention balance, δE ≤ T δS, as a two-way implication given a single disclosed identification. On this base, we assemble the mass chain retention → degree → curvature → internal-frequency ceiling → τc → m, with exactly one disclosed identification, τc = 1/ωint, yielding a curvature-limited mass bound m ≤ (ℏ/2c²) √((2K/M)(4 − Fmin)), whose contrapositive states that sufficiently large mass forces negative combinatorial curvature. We then read special and general relativity as the economics of retained distinctions — no universal reader, congestion of local update budgets, geometry as ledger — and mass as a distinction addressed to itself. To our knowledge, no other discrete-gravity programme — causal sets, Regge calculus, or hypergraph dynamics — possesses a machine-checked kernel of any size; here the entire supporting chain is one. Interpretive claims are tagged and separated from theorems throughout; the axiomatic basis is stated explicitly, the assembly is audited for circularity, and the open remainder is enumerated by name. Nothing in this note claims a derivation of the Einstein field equations; what is claimed is a theorem-anchored precursor with every non-theorem joint disclosed.