classCoeff_gaugePart_axis
plain-language theorem explainer
For each of the fifteen Freudenthal edge classes in 4D, the squared-length coefficient of the pure-gauge matrix built from the axis wave and axis gauge vector equals twice the indicator that the class carries bit 0. Cited by anyone evaluating the provisional finite TT quadratic or decoy-gauge loads on axis data. Proof rewrites by the general gauge loading identity, collapses both momentum and gauge dots against the class displacement by four-term simplification, then case-splits on the bit.
Claim. For every Freudenthal edge class $d$ among the fifteen nonzero displacements in $\{0,1\}^4$, if $H$ is the pure-gauge matrix $H_{ij}=m_i v_j+v_i m_j$ with axis wave $m=e_0$ and axis gauge vector $v=e_0$, then the class coefficient $D_d^\top H D_d$ equals $2$ when class $d$ has the zeroth coordinate bit set and equals $0$ otherwise.
background
This module is the 4D Regge edge stencil: fifteen Freudenthal-style edge classes given by the nonzero vectors in ${0,1}^4$, indexed by bit masks. For a symmetric $4\times 4$ matrix $H$ and class displacement $D$, the class coefficient is the squared-length load $D^\top H D$, the 4D analogue of the 3D polarized edge coefficient. The provisional finite TT quadratic sums squares of these coefficients with all-ones weights (true 4D Regge weights remain open).
A pure-gauge matrix is $\mathrm{gaugePart}(m,v)_{ij}=m_i v_j+v_i m_j$. The general gauge-loading identity states that its class coefficient is exactly $2(m\cdot D)(v\cdot D)$. Here the wave and gauge vectors are both the axis unit $e_0=(1,0,0,0)$, so each dot product against $D$ collapses to the $0$-component of $D$, i.e. the bit-0 indicator of the class.
Upstream, the edge TT decomposition layer supplies the axis wave and the gauge-part constructor used throughout the 4D attachment and stencil chain.
proof idea
One rewrite applies the general gauge-loading identity, reducing the claim to $2(m\cdot D)(v\cdot D)$ with $m=v=e_0$. Two short calculations evaluate the four-term sums: $m\cdot D$ and $v\cdot D$ each equal the bit-0 indicator of class $d$, by unfolding the axis vectors, the class displacement, and summing over $\mathrm{Fin},4$. After substituting both identities, a case split on whether bit 0 is set finishes with elementary arithmetic ($2\cdot 1\cdot 1=2$ versus $2\cdot 0\cdot 0=0$).
why it matters
Exact axis evaluation of pure-gauge class coefficients is the arithmetic kernel behind the module's nonvacuity and decoy checks. Downstream, it feeds the identity that the provisional finite TT quadratic on this pure-gauge input equals 32, and the bilinear pairing of axis TT-plus against the same gauge matrix vanishes termwise. The flat 4D Hessian assembly reuses it to identify decoy-gauge class coefficients with twice the bit-0 indicator.
In the QG full-theory campaign this sits after Regge edge TT attachment: it records honest gauge entry into the provisional aggregate (which is not identically gauge-invariant under all-ones weights). It does not close true Regge weight derivation, Einstein-Hilbert convergence, or the ledger name for full edge TT decomposition. Framework-wise it is discrete gravity bookkeeping on the 4D Freudenthal torus, not a forcing-chain (T0-T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.