recognitionLedgerCert
plain-language theorem explainer
Packages four structural facts about recognition ledgers on a finite lattice: a flat ledger exists, its total cost is zero, every total cost is nonnegative, and total cost vanishes exactly when the ledger is flat. Gravity and ledger-bookkeeping arguments cite this certificate rather than the four lemmas separately. The body is a field-by-field assembly of already-proved facts (flatLedger, flatLedger_totalCost_zero, totalCost_nonneg, totalCost_eq_zero_iff_flat).
Claim. There is a certificate asserting: (i) every finite lattice $\Lambda$ admits a recognition ledger; (ii) the flat (identically zero) ledger on $\Lambda$ has total cost $0$; (iii) for every recognition ledger $L$, the total cost satisfies $\sum_{i,j} L(i,j) \ge 0$; (iv) $\sum_{i,j} L(i,j) = 0$ if and only if $L$ is flat ($L(i,j)=0$ for all pairs).
background
In Recognition Science gravity the recognition ledger is the discrete bookkeeping object behind the gravitational action, the Page curve, and vacuum energy. On a finite substrate lattice $\Lambda$, a ledger is a map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ that is symmetric, vanishes on the diagonal, and obeys RCL subadditivity: $\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$ with gate $R(u,v)=2uv+2u+2v$ forced by the Recognition Composition Law.
Derived scalars are the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and the cell deficit $\Delta_i=\sum_j\mathcal{L}(i,j)$. Flatness means $\mathcal{L}\equiv 0$. The zero ledger flatLedger is the constant-zero cost function; it satisfies all ledger axioms by direct check. Upstream, totalCost_nonneg and totalCost_eq_zero_iff_flat already establish nonnegativity of the sum and the characterization that the sum vanishes exactly on flat ledgers (via nonnegativity of each summand).
proof idea
Pure structure inhabitation: each of the four fields of RecognitionLedgerCert is filled by an existing lemma. Existence of a ledger is witnessed by flatLedger Λ. Vanishing total cost of that witness is flatLedger_totalCost_zero. Nonnegativity of total cost for an arbitrary ledger is totalCost_nonneg. The zero-cost characterization is totalCost_eq_zero_iff_flat. No new algebra is performed.
why it matters
Gives a single named certificate that the recognition-ledger layer is inhabited and that total cost behaves as a genuine nonnegative defect measuring departure from flatness. Downstream, recognitionLedgerCert_inhabited is the one-line Nonempty proof that quotes this value, and the module's "RECOGNITION LEDGER ONE-STATEMENT" summary sits on top of that inhabitance.
In the framework this underwrites the three uses listed in the module doc: continuum limit of hinge-restricted total cost as Regge action, radiation entropy from bipartition boundary cost, and vacuum energy as ground-state total cost. Flatness as the unique zero-cost configuration is the discrete analogue of a recognition ground state (cf. the cosmology equilibrium slogan that zero total cost means consensus). It does not itself invoke T5–T8, but it is the bookkeeping substrate those forcing steps act on when gravity is derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.