rectangleShearPotential_strains
plain-language theorem explainer
The four-cell rectangle shear potential realizes pure shear: opposite edge differences equal +h and −h. Anyone proving shear visibility on the corrected J-ledger bridge or positivity of quadratic hinge energy cites this evaluation. The proof unfolds the potential definition and closes Fin-4 literal cases by decide plus norm_num.
Claim. For every real $h$, the rectangle shear potential $f_h$ on the four cells $\{0,1,2,3\}$ satisfies $f_h(0)-f_h(1)=h$, $f_h(2)-f_h(3)=h$, $f_h(1)-f_h(2)=-h$, and $f_h(3)-f_h(0)=-h$. Horizontal strains are $+h$; vertical strains are $-h$.
background
Lane 1b of Seven Gaps rebuilds the ledger-to-geometry bridge after the signed-deficit form was ruled out. Ledger costs are nonnegative and even in the deformation, while signed Regge deficits are odd; the honest geometric target is therefore the curvature-quadratic energy $\sum_h A_h,\delta_h^2$.
Both sides are defined separately. The geometric side uses only hinge areas and deficits. The ledger side uses a cell potential $f$ and the J-cost on coboundary strains $s_{ij}=f(i)-f(j)$. Coboundary strains obey the multiplicative cocycle, so RCL subadditivity follows from the d'Alembert identity $J(xy)+J(x/y)=R(J(x),J(y))$ with $J(x/y)\ge 0$. General antisymmetric strains can break the RCL gate, so the construction is scoped to coboundaries.
The rectangle shear potential is the four-cell witness for pure shear (horizontal $+h$, vertical $-h$). Its edge differences feed both the ledger total cost and the quadratic hinge energy.
proof idea
Tactic proof by direct evaluation. Six Fin-4 literal disequalities ($0\ne 1$, $0\ne 3$, $2\ne 1$, $2\ne 3$, $1\ne 3$, $3\ne 1$) are discharged by decide. Unfolding the potential definition reduces each difference to a concrete arithmetic expression in $h$; norm_num with those disequalities closes all four conjuncts. No external lemmas beyond the definition itself.
why it matters
This is the strain-pattern certificate for the pure-shear rectangle. Downstream, rectangleShear_ledgerEnergy_pos uses the first difference to show the horizontal cell cost is $J(e^h)=\cosh h-1>0$ for $h\ne 0$, so shear is visible to the corrected J-ledger (the transverse-traceless sector on which the conformal-average ansatz was proved blind). The twin geometric theorem rectangleShear_quadraticEnergy_pos uses the same differences to get strictly positive quadratic hinge energy.
In the Recognition framework this closes the shear half of the corrected bridge: ledger and geometry both see pure shear, matching the discrete Isaacson-type energy rather than the failed signed-deficit form. It does not yet settle the open Hessian-symbol comparison against independently derived Regge geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.