flatLedger
plain-language theorem explainer
The flat recognition ledger on any finite substrate lattice assigns zero cost to every cell pair. Gravity and vacuum-energy arguments cite it as the Minkowski baseline: total cost vanishes and the lattice is flat. Construction is immediate: constant-zero cost meets symmetry, diagonal vanishing, non-negativity, and RCL subadditivity by reflexivity and arithmetic.
Claim. For any finite lattice $\Lambda$, the flat ledger is the recognition ledger whose pairwise cost is identically zero: $\mathcal{L}(i,j)=0$ for all cells $i,j\in\Lambda$.
background
The recognition ledger is the central bookkeeping object of recognition gravity. On a finite substrate lattice $\Lambda$, it is a map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ giving the accumulated recognition cost of comparing cells $i$ and $j$. The continuum limit of total ledger cost on codimension-2 hinges recovers the Regge action; vacuum energy is the ground-state total cost; Page-curve entropy uses bipartition boundary costs.
Four axioms define a ledger: symmetry $\mathcal{L}(i,j)=\mathcal{L}(j,i)$; diagonal zero $\mathcal{L}(i,i)=0$; non-negativity; and RCL subadditivity $\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$ for the forced gate $R(u,v)=2uv+2u+2v$ coming from the Recognition Composition Law. Flatness means every cost vanishes.
Upstream cost notions (observer J-cost, multiplicative-recognizer derived cost, rung-coarsened sums) supply the same non-negative scalar that the ledger packages pairwise. Reflexivity of $\le$ on the arithmetic side discharges the zero lower bound.
proof idea
Field-by-field structure instance. Cost is the constant function $0$. Symmetry and diagonal zero are rfl. Non-negativity is le_refl 0. RCL subadditivity unfolds the gate $R$ and reduces $0\le R(0,0)$ by norm_num. No external ledger lemmas are needed.
why it matters
Supplies the canonical zero section of the ledger type. Downstream, flatLedger_isFlat records that it meets the flatness predicate, and flatLedger_totalCost_zero shows total cost vanishes (via the iff with flatness). Both feed RecognitionLedgerCert and the packaged one-statement: a flat ledger exists on every finite lattice, total cost is non-negative and zero iff flat (Minkowski). That one-statement is the structural theorem of the module (0 sorry, 0 RS-internal axiom).
In the Seven Gaps line, the flat ledger is the second encoding in value_route_is_encoding_choice: one encoding reads the symmetry-factor measure off off-diagonal cost, while the flat encoding returns zero, showing the value route is an encoding choice rather than a substrate derivation. Framework role: vacuum ledger cost as ground state, and the flat (Minkowski) baseline against which deficits and Regge-type action are measured.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.