LedgerBridgeNoGoStatus
plain-language theorem explainer
Documentation record packing three Boolean status flags for the ledger-to-hinge bridge no-go: sign obstruction proved, parity obstruction proved, and the corrected bridge target identified as curvature-quadratic energy. Downstream code cites the canonical instance with all flags true. There is no proof body; the structure is a typed checklist whose meaning is carried by the sibling obstruction theorems.
Claim. A status record with three Boolean fields: (i) the sign no-go is proved for every specification whose comparison-map image contains a strictly negative geometric deficit; (ii) the parity no-go is proved for every parity-covariant $J$-ratio ledger family (no signed linear-response deficit); (iii) the corrected bridge target is the nonnegative curvature-quadratic energy $\sum_h A_h\cdot\delta_h^2$, not the raw signed deficit $\sum_h A_h\cdot\delta_h$.
background
Lane 1a of the Seven Gaps gravity program studies the assumed substrate-to-triangulation bridge that equates recognition-ledger cell deficit with a raw geometric hinge deficit. The ledger deficit is a sum of $J$-costs and is therefore nonnegative. Weak-field Regge deficit angles are signed, so two-sided deformation classes contain hinges of strictly negative deficit.
Separately, any ledger built from $J$-costs of comparison ratios inherits $J(x)=J(1/x)$. Under the natural ratio parity $r(-\varepsilon)=r(\varepsilon)^{-1}$ (e.g. exponential strain), the induced deficit is even in the deformation parameter, with $O(\varepsilon^2)$ leading term, while the signed Regge response is odd and $O(\varepsilon)$.
This structure does not restate those theorems. It is a documentation checklist whose three flags point at the sign obstruction, the parity obstruction, and the geometric revision that the honest bridge target is the quadratic energy built in the companion LedgerEnergyBridge lane.
proof idea
No proof. The declaration is a structure of three Bool fields with field doc-comments. Mathematical content lives in the sibling theorems: bridge_forces_nonneg_geometricDeficit and no_bridge_matches_negative_deficit_spec for the sign flag; jRatioDeficit_even, ledger_family_deficit_even_of_ratio_parity, and no_ledger_family_linear_response for the parity flag; the quadratic-energy revision is a geometric premise recorded as the third flag. The canonical inhabitant sets every field to true by rfl.
why it matters
Closes the status surface of Lane 1a: after the two obstruction theorems rule out the assumed raw-deficit bridge form on negative-image specs and on parity-covariant $J$-ratio families, this record packages what is proved versus what remains a geometric premise. The sole downstream consumer is the canonical instance with all three flags true.
In the Recognition gravity program this forces a reading revision: the honest ledger-to-geometry bridge target is the nonnegative curvature-quadratic energy $\sum_h A_h\cdot\delta_h^2$ (deliverable B), not $\sum_h A_h\cdot\delta_h$. The composite claim that the assumed form is unsatisfiable on two-sided weak-field Regge classes still relies on the unformalized geometric premise that such classes carry negative image deficits and odd leading response. The structure makes that split explicit for auditors.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.