SubstrateBipartition
plain-language theorem explainer
A finite substrate lattice is split into complementary interior and exterior cells that cover the whole lattice and do not overlap. In recognition gravity this bipartition is the discrete stand-in for a horizon. Anyone defining boundary (horizon) ledger cost or Page-curve tracing cites it. As a structure it is pure data plus two partition axioms; there is no proof body.
Claim. For a finite substrate lattice $\Lambda$, a substrate bipartition is a pair of finite subsets $I,E\subseteq\Lambda$ such that $I\cup E=\Lambda$ and $I\cap E=\emptyset$. The interface between $I$ and $E$ is the discrete horizon.
background
The Recognition Ledger module treats gravity as bookkeeping on a finite substrate lattice $\Lambda$. A recognition ledger assigns to each ordered pair of cells a non-negative cost $\mathcal{L}(i,j)$ built from the J-cost of their comparison, subject to symmetry, vanishing diagonal, and RCL subadditivity via the forced gate $R(u,v)=2uv+2u+2v$.
Derived global quantities include total ledger cost, per-cell deficit, and flatness ($\mathcal{L}\equiv 0$). The continuum limit of total cost on codimension-2 hinges is intended to recover the Regge action; vacuum energy is the ground-state total cost; radiation entropy for the Page curve comes from tracing across a horizon cut.
A bipartition supplies that cut: interior versus exterior cells. Upstream cost notions (observer J-cost, multiplicative-recognizer cost, PRC quotient cost, rung-coarsen weighted sums) all feed the same non-negative pairwise ledger entries that will later be summed across the cut.
proof idea
No proof: this is a structure definition. It packages two Finset fields (interior, exterior) together with the two standard partition propositions (union equals the universe, the two sets are disjoint). Downstream definitions and theorems simply project these fields and use the axioms when rewriting sums over the cut.
why it matters
This is the discrete horizon type for recognition gravity. boundaryCost sums ledger entries from interior to exterior and is explicitly the ledger analogue of the boundary term in the gravitational action; non-negativity and interior/exterior symmetry are immediate corollaries. HorizonLedgerPreflight then scales ledgers continuously while preserving axioms, proving that positive horizon boundary cost admits no uniform spectral gap (P1 verdict: discrete-lattice capital does not quantize horizon cost). That preflight sits inside the seven-gaps gravity program and supports the module's three uses of the ledger: Regge-type action, Page-curve tracing across a horizon, and vacuum ledger cost. The structure itself does not invoke T5–T8 or the mass ladder; it only supplies the cut those arguments need.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.