Pith. sign in
theorem

twoHingeWitness_ledger_deficit_even

proved
show as:
module
IndisputableMonolith.Gravity.SevenGaps.RecognitionRatioBridge
domain
Gravity
line
237 · github
papers citing
none yet

plain-language theorem explainer

The recognition-ledger deficit induced by the exact unit-coupled two-hinge witness is even under sign flip of the deformation parameter. Anyone reconciling the paper's odd log-ratio bridge with the ledger sign and parity no-gos would cite this. The proof is a direct term application of the family parity theorem, using ratio covariance from the witness x-ratio negation lemma.

Claim. For every real $d$ and every hinge $\sigma \in \{0,1\}$, the recognition-ledger deficit at $\sigma$ of the ledger induced by the exact unit-coupled two-hinge recognition-ratio bridge at $-d$ equals the corresponding deficit at $+d$.

background

Phase 0a of Seven Gaps encodes the paper's odd substrate-to-geometry bridge: at each hinge $\sigma$, $\log x_\sigma = \kappa_\sigma \delta_\sigma +$ remainder with a cubic mesh remainder bound. That is an admissibility clause on a positive comparison ratio $x_\sigma$, not an equality of nonnegative deficits. The older bridge form (ledger deficit equals signed geometric hinge deficit) was refuted: ledger deficits are nonnegative, and J-ratio deficits are even in the deformation parameter, while signed Regge response is odd.

The two-hinge witness is an exact (remainder bound zero), unit-coupled ($\kappa=1$) bridge on $\mathrm{Fin},2$ with geometric deficits $d$ and $-d$. It induces a genuine recognition ledger whose cell costs are J-costs of ratio quotients (via the coboundary strain ledger). The family parity theorem states that any ledger family whose pairwise ratios flip to their inverses under $\varepsilon\mapsto -\varepsilon$ has even deficit under that flip. The witness supplies that ratio parity because each $x$-ratio entry negates in the log sense under $d\mapsto -d$.

proof idea

One-shot term proof: apply ledger_family_deficit_even_of_ratio_parity to the family $\varepsilon \mapsto$ ledger of the two-hinge bridge at $\varepsilon$. Supply the pairwise ratio map $r(\varepsilon;i,j)=x_i(\varepsilon)/x_j(\varepsilon)$, positivity from the bridge's positive $x$-ratios, and the cost identity that the induced ledger cost equals the J-cost of that ratio. The parity hypothesis is discharged by rewriting both numerator and denominator via the witness $x$-ratio negation lemma, then simplifying with inverse-of-quotient identities so the flipped ratio equals the reciprocal of the unflipped ratio. Instantiate at $d$ and hinge $\sigma$.

why it matters

This is the even-half of the deficit-observable separation that reconciles the paper with the no-gos. The sole downstream consumer is ratioBridge_separates_deficit_observables, which packages: signed geometric deficits $d$ and $-d$ (forbidden for ledger deficit by the sign no-go), together with an induced ledger whose deficit is nonnegative at every cell and even under $d\mapsto -d$. The no-gos constrain the ledger observable; the odd bridge stores signed content in $\log x$. Without this evenness fact, the witness would not close the parity side of that reconciliation. It sits in Gravity/SevenGaps Phase 0a and does not itself touch T5–T8 or the mass ladder; it clears a consistency obstruction so later geometric forcing can use the paper's bridge form without contradicting ledger nonnegativity.

Switch to Lean above to see the machine-checked source, dependencies, and usage graph.