bridge_forces_nonneg_geometricDeficit
plain-language theorem explainer
Any ledger-to-hinge bridge that matches cell deficits forces the geometric deficit to be nonnegative on the image of the comparison map. Gravity and RS auditors cite it as the positive half of the sign no-go against raw deficit matching. The proof is a one-line rewrite through the bridge equation plus nonnegativity of ledger deficits (sums of J-costs).
Claim. Let $L$ be a recognition ledger on a finite cell set $\Lambda$, and let $B$ be a ledger-to-hinge bridge from $L$ into a hinge space. Then for every cell $i\in\Lambda$, the geometric deficit of $B$ evaluated at the comparison image of $i$ satisfies $0\le \delta_B(x_\sigma(i))$.
background
Lane 1a of the Seven Gaps campaign targets the assumed substrate-to-triangulation bridge: it equates the recognition-ledger deficit at each cell with a raw geometric hinge deficit. The ledger deficit is built from the RS cost $J$, with $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$), so every cell deficit is a sum of nonnegative $J$-costs and is therefore nonnegative.
A ledger-to-hinge bridge packages a comparison map $x_\sigma$ from cells to hinges together with a geometric deficit assignment, under the matching hypothesis that geometric deficit at $x_\sigma(i)$ equals the ledger deficit at $i$. Weak-field Regge deficits are signed; two-sided deformation classes contain strictly negative hinges. The present statement is the positive half of that clash: matching forces nonnegativity on the comparison image.
The companion nonexistence form then rules out any specification that places a negative value on that image. The geometric premise that faithful comparisons hit negative hinges remains prose-tier and is not formalized in this module.
proof idea
Term-mode, two steps. Rewrite the goal geometric deficit at $x_\sigma(i)$ via the bridge matching equation, which identifies it with the ledger deficit at cell $i$. Discharge the rewritten goal by the ledger lemma that every cell deficit is nonnegative (as a sum of $J$-costs). No case splits or arithmetic beyond that transport.
why it matters
This is the load-bearing positive form of the sign obstruction in Gravity Lane 1a. It feeds the nonexistence companion: no bridge can realize a specification with a strictly negative geometric deficit on the comparison image. The campaign ledger anchors Gap 1 by re-deriving exactly this universal nonnegativity statement, so the flag cannot drift from the artifact.
Downstream ratio-bridge and two-cell witness developments use the same obstruction cluster when they exhibit even (parity-covariant) ledger deficits against odd linear Regge response. In the broader RS picture the nonnegativity is forced by the $J$-cost uniqueness (forcing chain T5) and the Recognition Composition Law structure of ledger costs; the no-go therefore blocks raw deficit-matching as a gravity bridge without touching the separate parity no-go or the unformalized geometric premise about two-sided weak-field classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.