strainHingeAreas
plain-language theorem explainer
Uniform hinge-area assignment on the ordered-pair set Λ×Λ: every pair gets area 1/2. Geometric bookkeeping so that an ordered-pair sum reproduces weight 1 per unordered hinge. Cited by the canonical ledger-to-quadratic-energy bridge and by the identity that turns quadratic curvature energy into half the double sum of squared potential differences. The body is the constant function 1/2.
Claim. For any cell type $\Lambda$, the strain hinge-area map $A:\Lambda\times\Lambda\to\mathbb{R}$ is the constant assignment $A(i,j)=1/2$ for every ordered pair $(i,j)$.
background
In the Seven Gaps Lane 1b module the corrected ledger-to-geometry bridge targets the nonnegative curvature-quadratic energy $\sum_h A_h,\delta_h^2$ (discrete Isaacson form), not a signed deficit match. The geometric side is defined purely from hinge areas and deficits; the ledger side is defined purely from a cell potential and the J-cost. Matching is proved only after both sides are built separately.
Hinges are the curvature-bearing codimension-2 strata (edges in a 3-simplicial ledger). Geometric deficit is the usual $2\pi-\sum\theta$. Here the hinge set is taken as the full ordered-pair product $\Lambda\times\Lambda$, so each unordered edge appears twice. Setting each ordered-pair area to $1/2$ makes the double sum carry the same total weight as unit area on unordered pairs.
Upstream continuum-bridge language identifies a weighted sum of squared potential differences with a hinge sum $\sum_h\delta_h A_h$; the present constant areas are the discrete bookkeeping choice that makes that identification clean for coboundary strains.
proof idea
Pure definition: the constant function sending every ordered pair to the real number $1/2$. No lemmas, no tactics.
why it matters
This is the area half of the canonical hinge data used throughout the corrected bridge. quadraticCurvatureEnergy_strainHinges unfolds it to prove that the quadratic curvature energy equals $(\sum_i\sum_j(f_0 i-f_0 j)^2)/2$. The same areas appear in canonicalQuadraticEnergyBridge, which packages base potential, small strain scale, areas $1/2$, and coboundary deficits into a LedgerToQuadraticEnergyBridge instance whose matching is already proved. rectangleShear_quadraticEnergy_pos uses them on $\mathrm{Fin},4$ to show the geometric side sees strictly positive energy under rectangle shear.
Framework role: after the signed-deficit no-go, the honest target is the quadratic energy; uniform ordered-pair areas are the minimal geometric input that lets the ledger J-cost of a coboundary strain match that energy in shape. The module still flags the OPEN Hessian-symbol comparison against independently derived Regge geometry; this definition only fixes the bookkeeping inside the shape-compatibility instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.