rectangleShearBridge
plain-language theorem explainer
Under the small-strain bound on scaled pair differences, the pure rectangle-shear cell potential on four sites yields a concrete ledger-to-quadratic-energy bridge. Gravity and discrete-geometry workers cite it as the canonical shear witness that both ledger cost and quadratic hinge energy are strictly positive. The body is a one-line wrapper feeding that potential into the canonical bridge constructor.
Claim. For $h,\varepsilon\in\mathbb{R}$ such that every scaled pair strain of the rectangle-shear potential on four cells satisfies $|\varepsilon\cdot(f_h(i)-f_h(j))|\le 1$, there is a ledger-to-quadratic-energy bridge on $\mathrm{Fin}\,4$: base potential $f_h$, deformation $\varepsilon$, hinge areas and deficits built from potential differences, with the proved two-sided matching $|\mathrm{totalCost}-(\varepsilon^2/2)S_2|\le(\varepsilon^4/2)S_4$.
background
Lane 1b of Seven Gaps corrects the ledger-to-geometry bridge after the signed-hinge no-go: ledger deficits are nonnegative and even in the deformation, while raw signed Regge response is odd. The honest geometric target is the curvature-quadratic energy $\sum_h A_h\delta_h^2$ (discrete Isaacson-type), defined from hinge areas and deficits alone.
The ledger side is the $J$-cost of a coboundary strain $s_{ij}=f_i-f_j$ for a cell potential $f$, with $J(x)=(x+x^{-1})/2-1$. Coboundary strains form a RecognitionLedger via the d'Alembert/RCL gate $J(xy)+J(x/y)=R(J(x),J(y))$; general antisymmetric strains can violate that gate.
LedgerToQuadraticEnergyBridge packages base potential, $\varepsilon$, the explicit small-strain hypothesis, hinge data, and the proved quadratic matching bound. The canonical instance builds hinge deficits from potential differences and unit areas on ordered pairs, certifying shape-compatibility of the two functionals rather than an independent Regge match.
proof idea
One-line wrapper: apply the canonical bridge constructor to the rectangle-shear potential at height $h$, the deformation $\varepsilon$, and the supplied small-strain hypothesis. All Prop fields of the bridge (matching bound, nonnegativity structure, coboundary ledger laws) are discharged inside that constructor; this definition only specializes the potential and the four-cell index type.
why it matters
Supplies the pure-shear witness named in the module status block: rectangle shear carries strictly positive ledger cost and positive quadratic hinge energy under the small-strain gate. That closes the THEOREM tier items on shear visibility and the canonical bridge instance for this configuration.
It sits downstream of the corrected bridge design forced by the signed-deficit no-go, and of the per-strain expansions $t^2/2\le J(e^t)\le(t^2/2)\cosh t$ with quartic remainder on $|t|\le 1$. Framework-wise it is geometry-side bookkeeping for Recognition gravity, not a forcing-chain (T0–T8) step.
No further used-by edges are recorded yet. The OPEN items remain: full Hessian-symbol comparison against frozen Regge on the periodic Freudenthal mesh, and multichannel escalation beyond the single coboundary channel. The MODEL identification of $\sum A_h\delta_h^2$ with continuum TT energy is definitional, not derived here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.