rectangleShear_quadraticEnergy_pos
plain-language theorem explainer
For any nonzero shear amplitude h, the quadratic hinge energy of the pure-rectangle shear configuration on four cells is strictly positive. Discrete-gravity and Recognition-ledger workers cite it as the geometric-side nondegeneracy witness for the corrected ledger-to-energy bridge. The proof is a short application of the general positivity lemma at hinge pair (0,1), reducing the nonzero-deficit check to h ≠ 0 via the explicit strain table.
Claim. For every real $h \neq 0$, the quadratic curvature energy built from the four-cell rectangle-shear hinge areas and hinge deficits is strictly positive: $0 < \sum_p A_p \, \delta_p^2$, where the areas and deficits come from the pure-shear rectangle potential of amplitude $h$.
background
Lane 1b of the Seven Gaps program replaces an unsatisfiable signed ledger-to-Regge bridge with a match to nonnegative curvature-quadratic geometric energy. The geometric functional is the discrete Isaacson-type sum $\sum_h A_h \delta_h^2$: hinge areas times squared deficits, with no ledger object in its definition.
The pure-shear rectangle configuration lives on four cells. Its cell potential produces pair strains that are $0$ or $\pm h$ (the explicit strain table). Hinge areas on ordered pairs are the constant positive weights used by the strain-hinge packaging; deficits are potential differences across those pairs.
A sibling positivity lemma already states that the quadratic energy is strictly positive whenever every area is positive and at least one hinge carries a nonzero deficit. This declaration specializes that lemma to the rectangle-shear data.
proof idea
One short refine of the general positivity lemma for quadratic curvature energy. Supply three ingredients: (i) every strain-hinge area is positive (unfold the constant area table and close by norm_num); (ii) the witness hinge is the ordered pair $(0,1)$ in $\mathrm{Fin},4$, whose area is likewise positive by norm_num; (iii) the deficit on that pair is nonzero. The last goal rewrites, via the rectangle-shear strain table, to $h \neq 0$, which is the hypothesis. No further analysis is needed.
why it matters
This is the geometric nondegeneracy half of the canonical shear bridge witness. Downstream, the rectangle-shear bridge packages the same potential into the corrected ledger-to-quadratic-energy bridge under the small-strain bound $|\varepsilon h| \le 1$. Without strict positivity of the geometric energy for $h \neq 0$, that instance would be vacuous on the curvature side.
In the broader Seven Gaps story, the old signed-deficit bridge is ruled out (ledger costs are even and nonnegative; signed Regge response is odd). The corrected target is the quadratic energy. This theorem confirms that pure shear is visible on that geometric side, so the shape-compatibility instance is not matching zero to zero. The remaining OPEN item in the module is the Hessian-symbol comparison against independently derived Regge geometry; this result does not close that flag, but it locks the shear witness used by the bridge instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.