twoCell_jRatioDeficit
plain-language theorem explainer
On the two-cell strain substrate, the J-ratio deficit at cell 0 equals cosh(ε·σ) − 1. That identity is the explicit parity witness: the deficit is even in the deformation parameter ε, O(ε²) at small strain, and carries no signed linear-response term. Anyone citing the ledger-bridge parity no-go uses it as the concrete two-cell evaluation. The proof is a direct two-term sum after substituting the strain values and applying J(exp t) = cosh t − 1.
Claim. For all real $\sigma$ and $\varepsilon$, the J-ratio deficit of the two-cell strain configuration of amplitude $\sigma$, at deformation parameter $\varepsilon$ and cell index $0$, equals $\cosh(\varepsilon\cdot\sigma)-1$.
background
Lane 1a of the Seven Gaps gravity work proves obstruction theorems against the assumed substrate-to-triangulation bridge that would equate recognition-ledger cell deficits with raw geometric hinge deficits. The ledger side is built from the J-cost $J(x)=(x+x^{-1})/2-1$, equivalently $J(e^t)=\cosh t-1$, which is nonnegative and symmetric under $x\mapsto 1/x$.
A one-parameter family of comparison ratios of exponential-strain type induces a cellwise J-ratio cost and a summed deficit. The two-cell strain configuration is the minimal substrate on which that deficit can be evaluated in closed form: one edge carries strain amplitude $\sigma$, the other is idle. The module's parity no-go then rests on showing that any such deficit is an even function of the deformation parameter $\varepsilon$, hence cannot match an odd (signed linear) Regge response except by vanishing.
Upstream, $J(1)=0$ and $J(e^t)=\cosh t-1$ are the Cost lemmas that turn the two-cell sum into a single hyperbolic identity.
proof idea
Evaluate the two strain entries of the two-cell configuration by norm_num: the $(0,0)$ entry is $0$ and the $(0,1)$ entry is $\sigma$. Unfold the deficit and the cell-cost definitions, then rewrite the Fin 2 sum. The idle edge contributes $J(e^{\varepsilon\cdot 0})=J(1)=0$ via Real.exp_zero and Jcost_unit0. The active edge contributes $J(e^{\varepsilon\cdot\sigma})$, which Jcost_exp_cosh rewrites as $\cosh(\varepsilon\cdot\sigma)-1$. The zero term drops by zero_add, leaving the claimed identity.
why it matters
This is the concrete two-cell parity witness named in the module doc-comment: the deficit is exactly $\cosh(\varepsilon\sigma)-1$, hence even in $\varepsilon$, with Taylor leading term $\tfrac12(\varepsilon\sigma)^2$ and no odd part. It underwrites the parity obstruction half of the ledger-bridge no-go (siblings such as the evenness of the J-ratio deficit and the exclusion of signed linear response for parity-covariant J-ratio families).
In the Recognition framework the point is structural, not numerical. Ledger deficits built from J-costs of comparison ratios inherit $J(x)=J(1/x)$ and, under ratio parity $r(-\varepsilon)=r(\varepsilon)^{-1}$, become even functions of strain. Weak-field Regge hinge response is odd at leading order. An even function matches an odd function only if both vanish, so the assumed raw-deficit bridge form cannot realize a signed linear geometric response on such families. The honest bridge target is therefore the nonnegative curvature-quadratic energy of the companion LedgerEnergyBridge lane, not a signed raw hinge deficit.
No downstream formal dependents are recorded yet; the theorem stands as the explicit evaluation that makes the parity reading checkable by hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.