orbitDeficit_dot_axisTTPlus
plain-language theorem explainer
For every S₄ hinge-orbit type, the star deficit class kernel is orthogonal to the plus TT polarization diag(0,0,1,−1) under the edge-class coefficient pairing. Gravity analysts assembling the zero-momentum 4D Regge Hessian cite this to kill the pure-TT deficit contribution before orbit weighting. The proof is a six-way case split reusing the four committed kernel evaluations, with types (2,1) and (3,1) reduced by complement transport.
Claim. For every hinge orbit type $\tau$, the edge-class pairing of the orbit deficit kernel $K_\tau$ with the plus transverse-traceless polarization $H_+=\mathrm{diag}(0,0,1,-1)$ vanishes: $\langle K_\tau,\,c(H_+)\rangle=0$.
background
This module assembles the committed per-orbit star deficit kernels with Heron area gradients into the flat second-variation class quadratic of the 4D Regge action at zero momentum (constant edge-class perturbation). Scope is per-cell Hessian only; finite-momentum Bloch phase folding remains open, and the campaign does not claim Einstein–Hilbert recovery.
The plus polarization $H_+$ is the unnormalized matrix $\mathrm{diag}(0,0,1,-1)$. The pairing classDot is the ordinary coefficient dot product of a $\mathrm{Fin},15$ class vector against the fifteen edge-class coefficients of a $4\times 4$ matrix. Orbit types run over the six $S_4$ hinge classes $(1,1)$, $(1,2)$, $(2,1)$, $(1,3)$, $(3,1)$, $(2,2)$; complement transport identifies the $(2,1)$ and $(3,1)$ kernels with the committed $(1,2)$ and $(1,3)$ kernels on edge classes.
Upstream, each of the four independent star kernels already evaluates to zero against $H_+$: the $(1,1)$ and $(2,2)$ proofs reduce via sign-kernel identities and integer class coefficients, while $(1,2)$ and $(1,3)$ are direct finite sums.
proof idea
Case-split on the six constructors of HingeOrbitType. Types $(1,1)$, $(1,2)$, $(1,3)$, and $(2,2)$ are one-line applications of the corresponding upstream theorems deficitKernel11_dot_axisTTPlus, deficitKernel12_dot_axisTTPlus, deficitKernel13_dot_axisTTPlus, and deficitKernel22_dot_axisTTPlus. Types $(2,1)$ and $(3,1)$ unfold the orbit kernel through the complement-transport equalities kernel21 and kernel31, then rewrite to the $(1,2)$ and $(1,3)$ evaluations respectively.
why it matters
This is the uniform deficit-side vanishing lemma that lets the zero-momentum true-weight Hessian kill $H_+$. Downstream, trueWeightZeroMomQuadratic_axisTTPlus sums orbit quadratics and obtains zero by feeding this lemma into orbitQuadratic_of_deficit_zero. The algebraic closer uses it the same way for fullMomentOrbitContribution_axisTTPlus. The Bloch-symbol module reuses it in foldOrbitAlong_axis_zero: at vanishing Bloch phase the fold reduces to the zero-momentum orbit quadratic, which is again zero by this pairing.
Within the QG full-theory campaign this is deliverable A item 5 on the TT axis: true orbit weights give a vanishing zero-momentum evaluation on the plus polarization. It does not close finite-momentum folding, nor S_RS_converges_EH_4d, nor gap_action_recovery. It is geometry-first: kernels and orbit counts come from the committed hinge modules, not reverse-engineered continuum weights.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.