jRatioDeficit
plain-language theorem explainer
Defines the J-ratio deficit at a cell as the sum of pairwise J-costs of exponential strain ratios under a one-parameter deformation. It is the raw, axiom-free analogue of the recognition-ledger deficit used in the ledger-to-hinge bridge no-go. Anyone citing the parity obstruction (even response, no signed linear term) uses this quantity. The body is a plain finite sum of cell-pair costs.
Claim. For a finite cell set $\Lambda$, a strain matrix $s:\Lambda\to\Lambda\to\mathbb{R}$, a deformation parameter $\varepsilon\in\mathbb{R}$, and a cell $i\in\Lambda$, the J-ratio deficit at $i$ is $\sum_{j\in\Lambda} J\bigl(\exp(\varepsilon\, s(i,j))\bigr)$, where $J$ is the recognition cost $J(x)=(x+x^{-1})/2-1$ (equivalently $\cosh(\log x)-1$ on positives). It is the sum of all cell-pair J-costs and needs no ledger axioms.
background
The module proves two obstruction theorems against equating recognition-ledger deficit with raw geometric hinge deficit (the assumed ledger-to-hinge bridge). Lane 1a splits into a sign no-go (ledger deficits are nonnegative sums of J-costs; weak-field Regge angles are signed) and a parity no-go (J-ratio families yield even response in the deformation parameter).
The recognition cost $J$ is the unique cost forced by the Recognition Composition Law: $J(x)=(x+x^{-1})/2-1$, with $J(x)=J(1/x)$ and $J\ge 0$. A J-ratio cell cost at pair $(i,j)$ is $J$ of the exponential strain ratio $\exp(\varepsilon, s(i,j))$. The present definition sums those pair costs over $j$ at fixed $i$, giving a raw analogue of RecognitionLedger.deficit that does not invoke ledger axioms.
Upstream cost constructions (observer forcing, multiplicative recognizers, PRC quotient cost) all specialize to this same $J$ on positive ratios, so the deficit inherits nonnegativity and ratio symmetry from the foundation layer.
proof idea
Pure definition: unfold to the finite sum $\sum_j$ of the sibling cell-pair cost jRatioCellCost s ε i j. No lemmas are applied at the definition site. Downstream evenness proofs simply unfold this sum and push the summand-wise identity jRatioCellCost_even through Finset.sum_congr.
why it matters
This is the working deficit for the parity half of the ledger-bridge no-go. It feeds three parent results in the same module: (1) jRatioDeficit_even, which states the deficit is even in $\varepsilon$ so the leading response is $O(\varepsilon^2)$, never the signed $O(\varepsilon)$ Regge linear term; (2) no_jRatio_deficit_linear_response, which rules out any match $\delta(\varepsilon)=c\varepsilon$ with $c\ne 0$ on a symmetric interval; (3) twoCell_jRatioDeficit, the two-cell witness that evaluates the deficit exactly to $\cosh(\varepsilon\sigma)-1$.
Together with the sign no-go (nonnegative ledger image versus signed geometric hinges), it blocks the assumed form of the substrate-to-triangulation bridge on two-sided weak-field deformation classes. The composite reading still relies on an unformalized geometric premise that faithful comparison maps hit strictly negative hinges and that weak-field Regge response is odd at leading order. Framework landmarks in play: T5 $J$-uniqueness and the RCL symmetry $J(x)=J(1/x)$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.