recognition_ledger_one_statement
plain-language theorem explainer
Four structural facts about the recognition ledger on any finite lattice: existence, zero total cost of the flat ledger, non-negativity of total cost, and vanishing of total cost exactly when the ledger is flat. Gravity and continuum-limit arguments that treat the ledger as gravitational bookkeeping cite this package. The proof is a four-component term applying the already-proved component lemmas.
Claim. For every finite lattice $\Lambda$: (i) a recognition ledger on $\Lambda$ exists; (ii) the flat (identically zero) ledger has total cost $0$; (iii) every recognition ledger $L$ satisfies $0 \le \mathrm{totalCost}(L)$; (iv) $\mathrm{totalCost}(L) = 0$ if and only if $L$ is flat (every pairwise cost vanishes).
background
The recognition ledger is the central bookkeeping object of recognition gravity. On a finite substrate lattice $\Lambda$, it is a cost 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 quantities are the total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$ and flatness (every pairwise cost zero). The module uses the ledger in three ways: continuum limit of hinge-restricted total cost recovers the Regge action; radiation entropy along a horizon boundary is a reduced von Neumann entropy; vacuum energy is the ground-state total cost on the full substrate.
Upstream, flatLedger supplies the zero cost map with all structure fields discharged by reflexivity and norm_num on the gate; isFlat is the pointwise-zero predicate; non-negativity of total cost and the zero-iff-flat equivalence are already proved in-module (and parallel non-negativity results exist for cosmological and SM-Lagrangian total costs).
proof idea
Term-mode four-fold conjunction. Existence is witnessed by ⟨flatLedger Λ⟩. Zero total cost of the flat ledger is flatLedger_totalCost_zero. Non-negativity is totalCost_nonneg. The characterization is totalCost_eq_zero_iff_flat. No new algebra: the statement only packages the four component results.
why it matters
This is the one-statement structural theorem of the recognition-ledger module (status: structural, zero sorry, zero RS-internal axiom). It records that the ledger is a well-posed, non-negative cost structure whose unique zero-cost state is the flat (Minkowski) ledger, which exists on every finite lattice.
Downstream the module positions the ledger as gravitational action (Regge limit on codimension-2 hinges), Page-curve bookkeeping (boundary bipartition costs), and vacuum-energy ground state. The RCL gate in the structure fields ties the ledger to the Recognition Composition Law and the forcing chain (T5 J-uniqueness). No used_by edges are recorded yet; the declaration is the export surface for those continuum and entropy arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.