LedgerToQuadraticEnergyBridge
plain-language theorem explainer
Bundles a coboundary strain (base potential f₀, scale ε, small-strain bound) with hinge areas and deficits so that ledger total cost equals ε² times quadratic curvature energy up to an explicit O(ε⁴) remainder. Gravity workers cite it as the corrected ledger-to-geometry interface after the signed-hinge no-go. It is a pure structure: data fields plus one proved two-sided matching inequality, no axioms.
Claim. A ledger-to-quadratic-energy bridge on a finite cell set $\Lambda$ consists of a base potential $f_0:\Lambda\to\mathbb{R}$, a deformation $\varepsilon\in\mathbb{R}$ with $|\varepsilon(f_0(i)-f_0(j))|\le 1$ for all cells, nonnegative hinge areas $A$ and hinge deficits $\delta$ on ordered pairs, such that $$\bigl|C_{\mathrm{tot}}(s_{\varepsilon})-\varepsilon^2 E_{\mathrm{quad}}(A,\delta)\bigr|\le \frac{\varepsilon^4}{2}\sum_{i,j}(f_0(i)-f_0(j))^4,$$ where $s_\varepsilon$ is the coboundary strain $\varepsilon(f_0(i)-f_0(j))$ and $E_{\mathrm{quad}}=\sum A\,\delta^2$.
background
Lane 1b of the Seven Gaps program replaces a refuted signed ledger-to-hinge bridge. Ledger deficits from the J-cost are nonnegative and even in the deformation parameter, while signed Regge hinge response is odd, so equality is impossible on two-sided weak-field classes (SevenGaps.LedgerBridgeNoGo). The honest geometric target is the nonnegative quadratic curvature energy $\sum_h A_h\delta_h^2$ (discrete Isaacson form).
The two sides are definitionally separate. Geometric energy is built only from hinge areas and deficits. Ledger total cost is built only from a coboundary strain $s_{ij}=f_i-f_j$ and the Recognition J-cost $J(x)=(x+x^{-1})/2-1$. Coboundary strains satisfy the cocycle identity on ratios and pass the Recognition Composition Law gate; general antisymmetric strains need not (general_antisymmetric_strain_can_violate_rcl).
The matching field is the two-sided bound linking those separate functionals under the explicit small-strain hypothesis that every scaled pair strain lies in $[-1,1]$.
proof idea
No proof body: this is a structure packing data and one Prop. The matching field is the statement that absolute difference between RecognitionLedger.totalCost of the coboundary strain ledger at scaled potential $\varepsilon f_0$ and $\varepsilon^2$ times quadraticCurvatureEnergy is at most $(\varepsilon^4/2)$ times the fourth-power sum of base potential differences.
Inhabitants discharge that field by the matching theorem coboundary_totalCost_quadratic_matching (and nonnegativity of areas by direct checks). Sibling bounds on $\cosh-1$ versus half-square remainders and J-cost expansions supply the analytic engine for that theorem; the structure itself only records the interface.
why it matters
This is deliverable B of the corrected bridge: the type that every proved ledger-to-geometry instance must inhabit. Downstream, canonicalQuadraticEnergyBridge builds a full instance for any coboundary configuration under small strain (areas $1/2$ on ordered pairs, deficits equal to potential differences, matching proved, no assumed fields). rectangleShearBridge specializes that to the pure-shear rectangle witness on Fin 4.
In the Recognition gravity stack it replaces the unsatisfiable signed-deficit bridge and aligns ledger energy with quadratic curvature energy, the weak-field object one expects from an Isaacson-type stress. Framework context: J-uniqueness (T5) and the RCL identity underwrite the ledger side; the eight-tick and $D=3$ forcing sit upstream of the discrete geometry this energy is meant to feed.
Honest limit recorded in the module: the canonical instance draws hinge data from the ledger potential itself, so it certifies shape-compatibility of the two functionals, not yet equality with independently derived Regge geometry (open Hessian-symbol comparison).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.