twoCellStrain
plain-language theorem explainer
Defines the two-cell antisymmetric strain matrix with off-diagonal entries ±σ and zero diagonal. It is the minimal substrate used to witness that J-ratio ledger deficits are even in the deformation parameter. Anyone citing the two-cell parity no-go against a signed linear Regge response needs this strain. The body is a pure case split on indices.
Claim. For any real strain amplitude $\sigma$, the two-cell strain is the map $s:\{0,1\}\times\{0,1\}\to\mathbb{R}$ with $s(i,i)=0$, $s(0,1)=\sigma$, and $s(1,0)=-\sigma$.
background
Lane 1a of the Seven Gaps program studies obstruction theorems against the assumed ledger-to-hinge bridge, which would equate recognition-ledger cell deficits with raw geometric hinge deficits. The ledger deficit is a sum of J-costs and is therefore nonnegative; weak-field Regge hinge deficits are signed.
The parity half of the no-go uses ratio families built from J-costs of comparison ratios. Because $J(x)=J(1/x)$, any one-parameter family obeying the natural ratio parity $r(-\varepsilon)=r(\varepsilon)^{-1}$ (e.g. exponential strain ratios $r=\exp(\varepsilon\cdot s)$) induces a deficit that is an even function of $\varepsilon$, with leading term $O(\varepsilon^2)$. The signed Regge response is odd and $O(\varepsilon)$.
This definition supplies the simplest antisymmetric strain $s$ on a two-cell substrate so that those parity identities can be evaluated in closed form.
proof idea
Pure definition by cases on the pair of Fin 2 indices: diagonal entries are zero; the (0,1) entry is $\sigma$; the (1,0) entry is $-\sigma$. No lemmas are applied.
why it matters
Feeds the two-cell parity witness twoCell_jRatioDeficit, which evaluates the J-ratio deficit at cell 0 under this strain and obtains exactly $\cosh(\varepsilon\cdot\sigma)-1$. That identity is even in $\varepsilon$, $O(\varepsilon^2)$ at small $\varepsilon$, and has no odd (signed linear-response) part.
Together with the evenness lemmas for J-ratio and ledger-family deficits, and the fact that an even function can match an odd function only if both vanish, it supports the parity no-go: no parity-covariant J-ratio ledger family realizes a signed linear-response deficit $\delta(\varepsilon)=c\cdot\varepsilon$ with $c\neq 0$. This is one of the two formalized obstruction pillars against the assumed form of the substrate-to-triangulation bridge in the Seven Gaps gravity lane.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.