ledgerBridgeNoGoStatus
plain-language theorem explainer
Canonical status record for the ledger-to-hinge bridge no-go: all three flags true (sign obstruction, parity obstruction, quadratic-energy corrected target). Gravity auditors cite it as the machine-checkable summary that Lane 1a closed its formal half. Construction is a pure structure instance with boolean literals; companion theorem discharges the flags by rfl.
Claim. The canonical ledger-bridge no-go status sets three booleans to true: (i) no bridge exists for any specification with a strictly negative deficit in the image of the comparison map; (ii) parity-covariant $J$-ratio ledger families admit no signed linear-response deficit; (iii) the corrected bridge target is the curvature-quadratic energy $\sum_h A_h\delta_h^2$, not the raw signed deficit $\sum_h A_h\delta_h$.
background
Lane 1a of the Seven Gaps 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 $J(x)=(x+x^{-1})/2-1$, hence nonnegative. Weak-field Regge hinge deficits are signed, so any faithful comparison map that hits a negative geometric deficit cannot match a ledger image.
Separately, $J$-ratio families with ratio parity $r(-\varepsilon)=r(\varepsilon)^{-1}$ induce an even deficit in the deformation parameter $\varepsilon$, while the leading Regge response is odd and linear. An even function matches a nonzero odd linear response only if both vanish. The status structure packages these two proved obstructions plus the reading that the right geometric target is quadratic energy, not signed deficit.
proof idea
No mathematical argument: the definition is a structure instance that hard-codes the three boolean fields to true. The companion theorem ledgerBridgeNoGoStatus_flags then proves each field equals true by three rfl steps. The actual no-go content lives in the upstream theorems named by the structure fields (sign obstruction via nonnegativity of ledger deficit; parity obstruction via evenness of $J$-ratio deficits).
why it matters
Closes the documentation half of Lane 1a: after the sign and parity no-gos are proved, this record is the single named object that says "all formal flags green." Downstream, ledgerBridgeNoGoStatus_flags re-exports the three equalities as a conjunction for status dashboards. Framework-wise it records the reading revision forced by the no-gos: the assumed linear hinge matching is unsatisfiable on two-sided weak-field classes, so the corrected bridge target is the curvature-quadratic energy $\sum_h A_h\delta_h^2$. The geometric premises (negative hinges in the image; odd linear Regge response) remain prose-tier and are not discharged here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.