LedgerToHingeBridge
plain-language theorem explainer
Packages the honest ledger-to-geometry interface: a map from substrate cells to hinges, a geometric deficit on hinges, and an explicit (underived) matching assumption that cell ledger deficits equal hinge geometric deficits. Gravity and SevenGaps authors cite it as the load-bearing bridge object. It is a structure definition, not a derived theorem.
Claim. Fix a finite substrate $\Lambda$ and a recognition ledger $L$ on $\Lambda$. A ledger-to-hinge bridge to a hinge type $H$ consists of a comparison map $x_\sigma:\Lambda\to H$, a geometric deficit $\delta:H\to\mathbb{R}$, and the explicit assumption that for every cell $i\in\Lambda$, the ledger deficit of $L$ at $i$ equals $\delta(x_\sigma(i))$. That matching is not forced by the ledger axioms alone.
background
The module records the machine-checked status of the link between the discrete recognition-ledger substrate and an effective geometric (hinge) description. A recognition ledger on a finite cell set $\Lambda$ carries a nonnegative cell deficit built from $J$-costs (equivalently the shifted cost $H(x)=J(x)+1=\frac12(x+x^{-1})$ obeying the d'Alembert form of the Recognition Composition Law). Ledger axioms give symmetry, diagonal zero, nonnegativity, and RCL-type subadditivity; they do not by themselves name a continuum geometry.
Hinges are the discrete stand-ins for local geometric degrees of freedom (strain or curvature-like data). The comparison map sends each substrate cell to the hinge whose deficit is to be compared with that cell's ledger deficit. The module's second finding, from the tensor shear sector, is that a pure conformal edge ansatz cannot realize nontrivial rectangle shear and therefore cannot recover transverse-traceless gravitational-wave modes; that obstruction motivates treating the ledger-geometry link as an assumed bridge rather than a conformal derivation.
proof idea
No proof body: this is a structure (data plus one Prop field). The three fields are the comparison map $x_\sigma$, the geometric deficit function, and bridge_assumed, the universal equality between ledger deficit at $i$ and geometric deficit at $x_\sigma(i)$. Downstream lemmas rewrite along that equality (for example replacing geometric deficit by ledger deficit to inherit nonnegativity). Nothing here derives the matching from ledger axioms; the field is deliberately tagged as assumed.
why it matters
This is the canonical interface object for the ledger-to-geometry gap in the Gravity domain. Downstream, the sign obstruction theorems use it directly: any such bridge forces nonnegative geometric deficit on the image of $x_\sigma$ (rewrite along the assumed match plus ledger deficit nonnegativity), and no bridge exists for a specification that assigns a strictly negative geometric deficit at some compared hinge. The campaign anchor re-derives that nonnegativity flag from this structure so gap-1 status cannot drift from the artifact. The energy bridge side uses related hinge deficit data for quadratic curvature energy identities.
In framework terms it separates what the recognition ledger actually proves from what must still be postulated to reach effective geometry. It does not close the full continuum limit; it makes the missing step explicit so conformal shortcuts and signed weak-field classes can be ruled out cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.