rectangleShear_ledgerEnergy_pos
plain-language theorem explainer
Pure rectangle shear with nonzero amplitude h produces strictly positive J-ledger total cost. Anyone citing the corrected ledger-to-geometry bridge or the shear-visibility gate needs this: the conformal ansatz was blind to TT shear, while the J-ledger is not. The proof isolates the horizontal edge cost J(exp h) = cosh h − 1 > 0 and lifts positivity through two nested nonnegative Finset sums.
Claim. For every real $h \neq 0$, the total recognition cost of the coboundary strain ledger built from the rectangle shear potential of amplitude $h$ is strictly positive: $0 < \mathrm{totalCost}(\mathrm{coboundaryStrainLedger}(f_h))$, where $f_h$ is that potential on four cells.
background
Lane 1b of Seven Gaps rebuilds the ledger-to-geometry bridge after the signed-hinge form was ruled out. Ledger deficits are nonnegative and even in the deformation; signed Regge response is odd. The corrected geometric target is the nonnegative quadratic curvature energy $\sum_h A_h \delta_h^2$.
The ledger side is definitionally separate: a cell potential $f$ induces coboundary strains $s_{ij} = f_i - f_j$, cell costs are $J(e^{s_{ij}})$ with $J(x) = (x+x^{-1})/2 - 1$, and total cost sums those nonnegative cell costs. The identity $J(e^t) = \cosh t - 1$ converts strain differences into hyperbolic cost. Coboundary scoping is essential: general antisymmetric strains can violate the RCL gate.
Rectangle shear is the pure transverse-traceless test configuration. Its potential differences on the four-cell complex include a horizontal edge of strain exactly $h$, so the corresponding cell cost is $\cosh h - 1$.
proof idea
Unfold total cost to a double Finset sum of cell costs. From the rectangle shear strain table, the $(0,1)$ potential difference equals $h$. Rewrite that cell cost via Jcost_exp_cosh as $\cosh h - 1$. Since $h \neq 0$, one_lt_cosh gives $\cosh h > 1$, hence the single cell cost is strictly positive.
Lift with Finset.single_le_sum twice: first the inner sum over $j$ at fixed $i=0$ is at least the positive $(0,1)$ term (all costs nonnegative), then the outer sum over $i$ is at least the positive $i=0$ row. Conclude by lt_of_lt_of_le.
why it matters
This is the shear-visibility gate for the corrected bridge. Downstream, rectangleShearBridge packages the same potential into a canonical LedgerToQuadraticEnergyBridge instance under a small-strain bound $|\varepsilon h| \le 1$. Together they show the pure-shear sector, on which the conformal-average ansatz is blind (conformal_ansatz_cannot_recover_gravitational_waves), carries strictly positive ledger energy and matches the quadratic geometric side in shape.
In the RS gravity program this closes the TT-sector half of the ledger-energy comparison: J-cost sees shear that conformal averaging erases. The remaining OPEN item in the module is the Hessian-symbol comparison against independently derived Regge geometry; this theorem only certifies positivity and bridge instantiability on the ledger-derived shear witness, not that external match. Landmarks in play are the unique J-cost (T5 / RCL) and the nonnegative quadratic energy target that replaced the failed signed-deficit bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.