classCoeff_axis0
plain-language theorem explainer
For any 4×4 matrix H, the Freudenthal edge-class coefficient at index 0 equals the quadratic edge load of H on the pure first-axis unit displacement. Gravity analysts packaging the 4D Regge TT stencil cite this to anchor the axis-aligned class among the 15 nonzero {0,1}⁴ displacements. The proof unfolds the class-coefficient definition and rewrites by the class-0 displacement identity.
Claim. For every real $4\times 4$ matrix $H$, the edge-class coefficient $c_0(H)=D^\top H D$ at Freudenthal class index $0\in\{0,\ldots,14\}$ equals the quadratic edge load of $H$ on the unit axis displacement $e_0=(1,0,0,0)$.
background
This module is the 4D Regge edge-stencil increment after ReggeEdgeTTAttachment4D: fifteen Freudenthal-style edge classes given by the nonzero displacement vectors in ${0,1}^4$, indexed by Fin 15 via bit masks. Per class one forms the squared-length coefficient $c_d(H)=D^\top H D$ (same convention as 3D polEdgeCoeff and 4D edge load) and a midpoint Bloch phase.
classCoeff H d is defined as edgeLoad H (classDisp d), where edgeLoad H D=\sum_{i,j} H_{ij} D^i D^j and classDisp builds the ${0,1}^4$ displacement from the class mask. The unit axis displacement axisDisp a is the standard basis vector $e_a$ on $\mathrm{Fin},4$. Upstream, classDisp_axis0 already proves that class $0$ has displacement exactly axisDisp 0.
The local campaign is honest about scope: class weights of the true 4D Regge Hessian at flat remain OPEN (provisional all-ones weights), and this file does not prove $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$ or full edge-TT decomposition.
proof idea
Short tactic proof. Unfold classCoeff, which is definitionally edgeLoad H (classDisp d). Rewrite the displacement via the already-proved identity classDisp_axis0 : classDisp 0 = axisDisp 0. The two sides become identical edge loads, and the goal closes.
why it matters
Pins the first of the fifteen Freudenthal edge classes to the pure $e_0$ axis edge, so axis-aligned loads in the 4D stencil match the attachment layer's edgeLoad/axisDisp API without an extra conversion. That alignment is needed for plane-wave midpoint packaging, the provisional finite quadratic aggregate $\sum_d c_d(H)^2$, and the exact gauge-entry identity $c_d(\mathrm{gaugePart},m,v)=2(m\cdot D)(v\cdot D)$ recorded in the module.
No downstream consumers are wired yet (used_by empty); the lemma is infrastructure inside the stencil file, sitting beside classCoeff_add, class-weight facts, and decoy evaluations (aggregate $8$ on axisTTPlus, $32$ pure gauge, $80$ pure trace). It does not touch T5–T8 forcing, RCL, or the $\phi$-ladder; it is pure discrete-gravity bookkeeping on the 4-cube. It also does not close the OPEN true-Regge class weights or flip gap_action_recovery.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.