RecognitionLedgerCert
plain-language theorem explainer
A master certificate packaging four structural facts about recognition ledgers on finite substrate lattices: existence of a flat ledger, vanishing total cost of the flat ledger, non-negativity of total cost, and the equivalence of zero total cost with flatness. Gravity and vacuum-energy arguments cite it as the one-statement interface for ledger bookkeeping. It is a pure structure definition whose fields are discharged by the concrete inhabitant recognitionLedgerCert.
Claim. A recognition-ledger certificate is a record of four statements, for every finite substrate lattice $\Lambda$: (i) there exists a recognition ledger on $\Lambda$; (ii) the flat (identically zero) ledger has total cost $0$; (iii) every ledger $L$ satisfies $0 \le \sum_{i,j} L(i,j)$; (iv) $\sum_{i,j} L(i,j) = 0$ if and only if $L$ is flat (every pairwise cost vanishes).
background
The module develops the recognition ledger as the central bookkeeping object of recognition gravity. On a finite substrate lattice $\Lambda$, a ledger is a cost map $\mathcal{L}:\Lambda\times\Lambda\to[0,\infty)$ that is symmetric, vanishes on the diagonal, and obeys RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$. The continuum limit of total ledger cost on codimension-2 hinges is intended to recover the Regge action; bipartition boundary costs model horizon terms for Page-curve bookkeeping; the vacuum energy is the ground-state total cost.
Derived quantities used here are the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and flatness: $\mathcal{L}\equiv 0$. The flat ledger is the zero cost function, which satisfies all ledger axioms. Upstream siblings already prove non-negativity of total cost and the equivalence of zero total cost with flatness; existence of a ledger is witnessed by the flat ledger itself.
proof idea
No proof body: this is a structure (certificate interface), not a theorem. The four fields are Prop-valued requirements quantified over finite decidable lattices. Downstream, recognitionLedgerCert fills them by pointing at flatLedger for existence, flatLedger_totalCost_zero for vanishing total cost, totalCost_nonneg for non-negativity, and totalCost_eq_zero_iff_flat for the zero-cost characterization. Inhabitation is then a one-line wrapper ⟨recognitionLedgerCert⟩.
why it matters
This is the §7 master cert for the recognition ledger: the single interface that packages existence, ground-state vanishing, positivity, and rigidity of the total cost. Downstream recognitionLedgerCert and recognitionLedgerCert_inhabited discharge it with zero sorry, matching the module status (structural theorem, no RS-internal axiom). Parent narrative uses the ledger in three gravity roles: continuum total cost as Regge action, bipartition boundary cost as horizon entropy bookkeeping, and vacuum energy as ground-state total cost. Within the broader RS chain, the cost values are instances of the J-cost forced at T5 and gated by the Recognition Composition Law; flatness is the zero-defect reference against which curvature and vacuum contributions are measured. The cert does not itself derive continuum gravity; it locks the discrete bookkeeping layer those limits sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.