ledgerBridgeNoGoStatus_flags
plain-language theorem explainer
Records that the three ledger-to-hinge bridge no-go status flags are all true: sign obstruction for negative-image deficit specs, parity obstruction for parity-covariant J-ratio families, and corrected target equal to quadratic energy. Anyone citing the Seven Gaps Lane 1a status board uses this. The proof is three reflexivity steps against the canonical status definition.
Claim. The canonical ledger-bridge no-go status record satisfies: the sign no-go is marked proved for specifications whose geometric deficit takes a strictly negative value on the comparison image; the parity no-go is marked proved for parity-covariant ledger families; and the corrected target is marked as quadratic energy.
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 hinge deficits are signed, so any faithful comparison map that hits a negative geometric deficit cannot be realized by such a bridge (sign no-go).
Separately, J-cost has the ratio symmetry $J(x)=J(1/x)$. Any one-parameter ratio family with $r(-\varepsilon)=r(\varepsilon)^{-1}$ therefore induces an even deficit in the deformation parameter, with leading $O(\varepsilon^2)$ term. Signed Regge linear response is odd in $\varepsilon$; an even function matches a nonzero odd linear response only if both vanish (parity no-go).
The status structure packages three boolean flags documenting that those two no-gos are proved in-module and that the corrected matching target is quadratic energy rather than a signed linear hinge angle. The upstream definition hard-codes all three flags to true.
proof idea
Pure documentation theorem. Unfold the canonical status definition (all three fields set to true) and close each conjunct by reflexivity: the term is $\langle \mathrm{rfl},,\mathrm{rfl},,\mathrm{rfl}\rangle$. No lemmas beyond definitional equality are used.
why it matters
Gives a single, machine-checkable status board for Seven Gaps Lane 1a so downstream gravity prose and audits can cite one object rather than re-inspecting the sign and parity obstruction theorems. Those obstructions (nonnegative ledger deficit versus signed Regge angles; even J-ratio response versus odd linear hinge response) force the corrected bridge target to be a quadratic energy functional, not a raw signed deficit. The module claims zero sorry and zero RS-internal axioms; this flag theorem is the explicit bookkeeping endpoint of that claim. No downstream Lean consumers are recorded yet; the value is audit and paper-facing status, not a new mathematical step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.