finiteTTQuadratic
plain-language theorem explainer
Provisional finite TT quadratic on 4D Regge edge classes: Q(H) is the sum of squared class coefficients over the fifteen nonzero {0,1}^4 displacements, with every weight set to 1. Gravity analysts cite it as the working aggregate while true 4D Regge flat-Hessian weights stay open. The body is a direct finite sum of squares of the edge loads D^T H D.
Claim. For a $4\times 4$ real matrix $H$, the provisional finite TT quadratic is $Q(H)=\sum_{d} c_d(H)^2$, summed over the fifteen nonzero displacement classes $D\in\{0,1\}^4$, where each class coefficient is $c_d(H)=D^\top H D$ and every provisional weight equals $1$.
background
This module is the 4D Regge edge-stencil layer after TT attachment: a kernel-checked packaging of Freudenthal-style edge classes on the 4-cube. The fifteen classes are the nonzero vectors in ${0,1}^4$, indexed by bit masks. Each class carries a coefficient $c_d(H)=D^\top H D$, matching the 3D polarized-edge and 4D edge-load convention.
The local campaign goal is a finite TT quadratic aggregate on those classes. True 4D Regge flat-Hessian class weights (the lift of the 3D hinge factor contracted with deficit incidence) are explicitly OPEN and must not be reverse-engineered from Einstein-Hilbert. Until they are derived, the provisional aggregate uses weight $1$ on every nonzero class.
Upstream, the only structural ingredient is the class coefficient itself: load the matrix $H$ on the class displacement. Naming collisions with the cost-algebra shift $H=J+1$ are unrelated; here $H$ is a $4\times 4$ matrix field.
proof idea
Pure definition: unfold to the finite sum over Fin 15 of the square of each class coefficient. No lemmas, no tactics, no proof obligations. Downstream identities (polarization, explicit evaluations on TT seeds and decoys) expand this sum and simplify the fifteen terms class by class.
why it matters
This is the working finite quadratic that every later stencil lemma quotes. Downstream it feeds the exact polarization identity, the evaluation $Q(\mathrm{axisTTPlus})=8$ with nonvanishing TT-seed certificate, and the decoy suite: pure gauge and pure trace hit the distinct predicted values $32$ and $80$. Continuum preflight uses those facts to record that the provisional weight-1 aggregate fails gauge invariance on a TT seed (exact identity $Q(\mathrm{gauge})=\sum 4(m\cdot D)^2(v\cdot D)^2$, not identically zero).
In the Recognition gravity campaign this is the 4D analogue of the 3D finite TT edge-class packaging. It does not close continuum recovery: module tags forbid claiming $S_{\mathrm{RS}}\to\mathrm{EH}_{4d}$, full edge-TT decomposition, or gap-action recovery. The OPEN item remains replacement of the all-ones weights by derived 4D Regge Hessian class weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.