edgeStrain
plain-language theorem explainer
Edge strain of a real 4×4 metric perturbation H along an integer 4-vector D is the quadratic form ∑_{i,j} H_{ij} D_i D_j. Gravity analysts cite it when assembling linearized strain currents on the Freudenthal 16-site patch and when weighting Regge couplings. The body is a plain double sum, copied to match the Regge-exact flat Hessian Bloch symbol without importing that chain.
Claim. For a real $4\times 4$ matrix $H$ and an integer displacement $D\in\mathbb{Z}^{4}$, the edge strain is $\sum_{i=0}^{3}\sum_{j=0}^{3} H_{ij}\,D_i\,D_j$.
background
This module freezes the linearized metric-null story on the Freudenthal cover: a sixteen-site binary hypercube patch in 4D (three spatial plus time), with edge currents built from metric perturbations. Mat4 is simply the type of real $4\times 4$ matrices; those matrices stand for linearized metric (or Hessian) data on the patch.
The integer vector $D$ is a site-to-site displacement in the four binary coordinates of the unit hypercube. Upstream, the same quadratic form appears as the edge strain in the Regge-exact flat Hessian Bloch-symbol analysis; this module redefines it locally so the finite edge-image development need not import that heavier chain. The module doc states the scope explicitly: linearized flat-patch metric perturbations via strain currents, with theorems aimed at nontriviality, symmetry, and properness against antisymmetric posting.
proof idea
Pure definition: expand the quadratic form as an explicit double sum over Fin 4, casting each integer component of $D$ to $\mathbb{R}$ and contracting against the matrix entries of $H$. No lemmas, no tactics.
why it matters
This is the atomic contraction that turns a metric matrix into a scalar on each directed edge. Downstream, strainCurrent sets the current between patch sites $i,j$ to the edge strain of $H$ along the patch displacement $j-i$; MetricEdgeImage is then the set of all such currents. Symmetry facts such as invariance under $D\mapsto -D$, the zero-current witness, and the explicit evaluation on the axis TT-cross mode all unfold through this sum.
On the Regge side, the same form reappears inside coupling weights as the product of strains on a pair of edge displacements, tying the finite patch image to the Bloch-symbol Hessian analysis. In the broader Recognition gravity stack this is the linearized, discrete stand-in for metric strain on the eight-tick / $D=3$ ledger geometry, scoped to the frozen Order-Sensitive Gravity proposition rather than full nonlinear curvature.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.