flatLedger_isFlat
plain-language theorem explainer
The zero ledger on any finite substrate lattice is flat: every pairwise recognition cost vanishes. Gravity and vacuum-energy arguments cite this as the canonical ground configuration. The proof is a one-line reflexivity on the constant-zero cost field.
Claim. For any finite lattice $\Lambda$, the zero recognition ledger $\mathcal{L}_0$ (with $\mathcal{L}_0(i,j)=0$ for all cells $i,j$) is flat: $\mathcal{L}_0(i,j)=0$ holds identically.
background
The recognition ledger is the bookkeeping object of recognition gravity: on a finite substrate lattice $\Lambda$, a ledger $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ records the accumulated recognition cost of each cell pair. Module conventions require symmetry, vanishing diagonal, non-negativity, and RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
Flatness means every entry is zero. The flat ledger is the structure whose cost field is the constant map $(i,j)\mapsto 0$, with the ledger axioms discharged by reflexivity and a one-line norm_num on the gate. Upstream cost notions (J-cost of recognition events, derived costs of multiplicative recognizers, rung-coarsened totals) all specialize to zero on this configuration.
Derived quantities include total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and cell deficits; the continuum limit of hinge-restricted total cost is identified with the Regge action.
proof idea
Term-mode proof. Unfolding flatness on flatLedger asks that the constant-zero cost field equal zero at every pair. That is definitional, so the proof is fun _ _ => rfl. No lemmas are invoked.
why it matters
This is the base case for ledger cost calculus in recognition gravity. Downstream, flatLedger_totalCost_zero obtains zero total cost by applying the equivalence "total cost vanishes iff the ledger is flat" to this theorem. That zero-total configuration is the vacuum ground state in the module's third use case (vacuum energy as ground-state total ledger cost over the substrate lattice) and the trivial endpoint of the gravitational-action story.
Within the broader RS chain it sits under the J-cost uniqueness (T5) and RCL gate structure already baked into the ledger axioms; it does not itself force $\phi$, the eight-tick period, or $D=3$. It closes no open scaffold: the module is already 0-sorry structural.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.