finiteTTQuadratic_neg
plain-language theorem explainer
The provisional finite TT quadratic on 4×4 matrices is even: replacing H by −H leaves the sum of squared edge-class coefficients unchanged. Anyone checking parity, gauge counterexamples, or polarization identities for the 4D Regge edge stencil will cite this. The proof is a one-line specialization of the scalar-homogeneity law at c = −1.
Claim. For every real $4\times 4$ matrix $H$, the provisional finite TT quadratic satisfies $Q(-H)=Q(H)$, where $Q(H)=\sum_{d=1}^{15} c_d(H)^2$ and $c_d(H)=D_d^{\mathsf T} H D_d$ runs over the fifteen nonzero $\{0,1\}^4$ Freudenthal edge-class displacements.
background
This module builds the 4D Regge edge stencil after the TT-attachment layer: fifteen Freudenthal-style nonzero displacement classes in ${0,1}^4$, plane-wave midpoint loads, and a provisional finite quadratic aggregate on those classes.
The aggregate is $Q(H)=\sum_d c_d(H)^2$ with provisional weights $w_d=1$ on every nonzero class (true 4D Regge flat-Hessian weights remain OPEN). Each class coefficient is $c_d(H)=D^{\mathsf T} H D$, the same bilinear convention as the 3D polarized edge coefficient and the 4D edge load.
Upstream, scalar homogeneity is already proved: $Q(c\cdot H)=c^2 Q(H)$. Evenness under $H\mapsto -H$ is the $c=-1$ case of that identity, needed before gauge-entry and nonvacuity checks that evaluate $Q$ on pure-gauge, pure-trace, and axis-TT inputs.
proof idea
One-line wrapper. Instantiate the already-proved scalar law $Q(c\cdot H)=c^2 Q(H)$ at $c=-1$, then rewrite $(-1)\cdot H$ as $-H$ and use $(-1)^2=1$. No unfolding of the fifteen-term sum is required.
why it matters
Evenness is the first algebraic sanity check on the provisional finite TT quadratic before gauge-entry identities and decoy evaluations in the same file. The module records that pure-gauge loads give $Q=\sum_d 4(m\cdot D)^2(v\cdot D)^2$ (not identically zero), while axis-TT, pure-gauge, and pure-trace inputs evaluate to the distinct values 8, 32, and 80; those comparisons tacitly use $Q(-H)=Q(H)$ so sign flips of the metric perturbation do not change the reported numbers.
In the QG campaign this sits one kernel-checked step after ReggeEdgeTTAttachment4D and packages the 4D analogue of the 3D finite TT edge-class block. It does not close the OPEN weight problem, does not prove $S_{\mathrm{RS}}$ converges to Einstein–Hilbert in 4D, and does not flip gap_action_recovery. No downstream consumers are wired yet; the lemma is local infrastructure for the stencil’s exact finite-difference layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.