RecognitionLedger
plain-language theorem explainer
A recognition ledger is a finite-lattice pairwise cost that is symmetric, diagonal-zero, nonnegative, and RCL-subadditive under the forced gate R(u,v)=2uv+2u+2v. Gravity modules cite it as the bare bookkeeping type for recognition gravity (action, Page curve, vacuum cost). Downstream dual-entry and hinge-bridge work treat it as the sign-blind shadow of richer strain states. As a structure it only packages those four axioms; there is no separate proof body.
Claim. A recognition ledger on a finite substrate lattice $\Lambda$ is a map $\mathcal{L}:\Lambda\times\Lambda\to\mathbb{R}$ such that $\mathcal{L}(i,j)=\mathcal{L}(j,i)$, $\mathcal{L}(i,i)=0$, $\mathcal{L}(i,j)\ge 0$, and $\mathcal{L}(i,k)\le R(\mathcal{L}(i,j),\mathcal{L}(j,k))$ for every intermediate cell $j$, where $R(u,v)=2uv+2u+2v$ is the RCL gate.
background
The module sets recognition gravity on a finite substrate lattice $\Lambda$ (a Fintype). The ledger $\mathcal{L}$ assigns to each cell pair the accumulated recognition cost of comparing them. In RS this cost is the J-cost lineage: $J(x)=(x+x^{-1})/2-1$ from T5 uniqueness, with the Recognition Composition Law forcing the binary gate $R(u,v)=2uv+2u+2v$ used in the subadditivity axiom.
Module conventions fix four properties: symmetry, diagonal zero (self-comparison costs nothing), nonnegativity, and RCL subadditivity through every intermediate cell. Derived quantities defined alongside include total ledger cost $\sum_{i,j}\mathcal{L}(i,j)$, cell deficit $\Delta_i=\sum_j\mathcal{L}(i,j)$, and flatness ($\mathcal{L}\equiv 0$).
Upstream cost constructions (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen multiset cost) supply the same nonnegative J-shaped scalar that the ledger fields axiomatize at lattice scale.
proof idea
Structure definition, not a proved theorem. The type packages five fields: the cost map and four Prop witnesses (symmetry, diagonal zero, nonnegativity, RCL subadditivity via the sibling gate $R$). No tactics or lemmas discharge anything; inhabitants are built by supplying a concrete cost and proving the four axioms, as in the flat (zero) ledger constructed immediately below.
why it matters
Central bookkeeping object of recognition gravity. The module uses it three ways: continuum limit of total cost on codimension-2 hinges recovers the Regge action; radiation entropy along a horizon is von Neumann entropy after tracing ledger cells; vacuum energy is the ground-state total cost on the full lattice.
Downstream, dual-entry enrichment treats the ledger as the bare, sign-blind shadow of oriented strain states: swap-even observables factor through the bare ledger, and no bare selector recovers the signed extract (enrichment strictly richer than the ledger). The ledger-to-geometry bridge consumes it as the discrete input to hinge geometry. Extensionality on equal cost maps is re-proved where enrichment needs ledger equality.
It sits after T5 J-uniqueness and the RCL gate; it does not itself force $\phi$, the eight-tick octave, or $D=3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.