strainCurrent
plain-language theorem explainer
Maps a 4×4 real metric perturbation to the induced edge strains on every pair of the sixteen-site Freudenthal patch. Gravity analysts cite it as the generator of the linearized metric edge image. The body is a one-line composition of edge strain with binary patch displacements.
Claim. For a $4\times 4$ real matrix $H$, the strain current is the map $(i,j)\mapsto$ the quadratic form of $H$ on the integer displacement between patch sites $i$ and $j$, for $i,j\in\{0,\ldots,15\}$.
background
The module freezes the linearized metric-null story from the order-sensitive gravity plan on the Freudenthal cover. The sixteen-site patch is the unit 4-cube with binary coordinates; displacements between sites are integer 4-vectors given by patchDisp.
A metric perturbation is a real $4\times 4$ matrix $H$. Edge strain is the quadratic form $\sum_{\mu,\nu} H_{\mu\nu} D_\mu D_\nu$ on an integer displacement $D$, matching the Regge flat-Hessian Bloch symbol. Strain current evaluates that form on every ordered pair of patch sites.
Upstream, the same edge-strain formula appears in the Regge exact flat Hessian analysis; the cost algebra $H$-reparametrization is imported only as ambient infrastructure and is not used in the body.
proof idea
Pure definition: apply edge strain of $H$ to the patch displacement between sites $i$ and $j$. No lemmas, no tactics.
why it matters
This is the generator of the finite linearized metric edge image: MetricEdgeImage F means $F$ equals the strain current of some $Mat4$ perturbation. Downstream theorems use it to prove symmetry of the current, nontriviality of the image (via the axis TT-cross example equaling 2 on sites 0 and 12), membership of that cross mode, and properness against elementary antisymmetric postings. It also feeds the order-sensitive history response argument that a configuration difference lies outside the image. In the RS gravity chain this pins the linearized flat-patch metric sector on the Freudenthal cover without importing the heavy analysis stack.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.