edgeLoad
plain-language theorem explainer
Quadratic edge loading of a Euclidean 4×4 matrix H against a displacement vector d is the bilinear form Σᵢⱼ Hᵢⱼ dᵢ dⱼ. Anyone working the 4D Regge TT/gauge attachment or the edge-class stencil cites it as the shared loading convention with the 3D polEdgeCoeff chain. The body is the literal double sum; no proof content.
Claim. For a real $4\times 4$ matrix $H$ and a displacement $d\in\mathbb{R}^4$, the edge load is $d^{\mathsf T} H d = \sum_{i=0}^{3}\sum_{j=0}^{3} H_{ij}\, d_i d_j$.
background
This module sits in the QG full-theory campaign (Wave 4 / lane W4-1), one step past the algebraic EdgeTTDecomposition4D layer. The goal is to attach the Euclidean 4×4 TT / gauge / transverse-trace split to plane-wave edge loadings on axis edges of the 4-torus.
The loading convention matches the 3D chain: the polarization edge coefficient is the same quadratic form $E\mapsto D^{\mathsf T} E D$. Here $H$ is any real 4×4 matrix (later specialized to TT projectors, gauge parts, or decoys), and $d$ is a discrete edge displacement in covering-space coordinates.
Upstream, the continuum plane-wave phase $k\cdot x$ and the eight-tick phase infrastructure supply the oscillatory layer that multiplies these loads; the present definition is purely algebraic and does not yet involve phases.
proof idea
Pure definition: expand the quadratic form as the double finite sum over Fin 4. No lemmas, no tactics. Sibling lemmas (edgeLoad_axis, edgeLoad_add, edgeLoad_smul, edgeLoad_neg, edgeLoad_sub) then record the elementary algebraic consequences (diagonal extraction on axis displacements, linearity).
why it matters
This is the shared kernel for every 4D edge-class coefficient. Downstream, classCoeff is literally edgeLoad H (classDisp d), and the axis/TT-plus/TT-cross/decoy-trace evaluations in ReggeEdgeStencil4D unfold through it. Inside this module it underwrites the plane-wave edge map, linearity transport of the TT decomposition across edges, and the exact finite-difference gauge↔discrete-Lie identity on axis edges.
It does not close the ledger name edge_tt_decomposition, nor continuum Einstein-Hilbert recovery, nor gap_action_recovery. It is the loading primitive those later steps must reuse if the 4D Regge stencil is to stay consistent with the 3D convention and with the Recognition forcing chain's discrete geometry (eight-tick octave, D=3 spatial plus time).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.