LedgerEnergyBridgeStatus
plain-language theorem explainer
A status record of honesty-tier flags for the corrected ledger-to-geometry energy bridge in Seven Gaps Lane 1b. Gravity auditors cite it to see which bridge claims are kernel theorems, which are modeling identifications, and which remain open. It is a pure structure definition; the canonical inhabitant sets five theorem flags true and leaves two open.
Claim. A record of boolean honesty flags for the ledger-energy bridge: theorem-tier flags for the two-sided quadratic expansion $t^2/2 \le J(e^t)=\cosh t-1 \le (t^2/2)\cosh t$ with quartic remainder on $|t|\le 1$; for coboundary-strain $J$-costs forming a recognition ledger; for RCL-gate failure on general antisymmetric strain; for quadratic matching with explicit quartic remainder; and for strictly positive pure-shear ledger energy; plus a model-tier flag for the Isaacson-type identification $\sum_h A_h\delta_h^2$; and open flags for Hessian-symbol comparison and tensor multichannel escalation.
background
Seven Gaps Lane 1b corrects the ledger-to-geometry bridge after a no-go: ledger deficits are nonnegative and even in the deformation, while signed Regge hinge response is odd, so raw signed matching is impossible. The honest geometric target is the nonnegative curvature-quadratic energy $\sum_h A_h\cdot\delta_h^2$ (discrete Isaacson-type form).
The two sides are definitionally separate. Geometric quadratic curvature energy uses only hinge areas and deficits. The ledger side uses coboundary strains $s_{ij}=f_i-f_j$ and the $J$-cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), with total cost summed over pairs. Matching links them; the canonical instance builds hinges from the ledger potential itself, so it certifies shape-compatibility, not yet independent Regge geometry.
Scoping is forced: coboundary strains satisfy the cocycle and the RCL gate via the d'Alembert identity $J(xy)+J(x/y)=R(J(x),J(y))$. General antisymmetric strains can violate the gate.
proof idea
No proof: this is a structure of eight Bool fields, each documented by honesty tier (THEOREM / MODEL / OPEN). Downstream, the canonical inhabitant ledgerEnergyBridgeStatus assigns true to the five theorem flags and the model flag, and false to the two open flags. The mathematical content lives in the sibling theorems named in the field docs (Jcost_exp_sub_half_sq_abs_le, coboundaryStrainLedger, rclGate_Jcost_eq, general_antisymmetric_strain_can_violate_rcl, coboundary_totalCost_quadratic_matching, shear-positivity lemmas).
why it matters
This is the module's honesty dashboard for the corrected bridge after LedgerBridgeNoGo. Downstream, ledgerEnergyBridgeStatus is the single canonical record consumers read to know what is proved versus modeled versus open.
It packages the T5 $J$-uniqueness and RCL infrastructure into a gravity-facing claim list: quadratic expansion of $J(e^t)$, coboundary-only ledger instance, forced scoping via gate failure, quadratic matching with quartic remainder, and shear visibility (pure rectangle shear has strictly positive ledger and quadratic hinge energy). The model flag isolates the Isaacson identification $\sum A_h\delta_h^2$ as definitional, not derived. The two open flags mark the remaining gaps: Hessian-symbol comparison to frozen Regge on the periodic Freudenthal mesh, and tensor multichannel escalation beyond one coboundary channel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.