ker_push_sqrt2_half
plain-language theorem explainer
Equates a real star-kernel sum over the 15 edge classes (with permuted Hessian coefficients and squared midpoint phases on symbolDir) to √2 times an integer certificate sum, divided by 8. Cited when discharging t12/t21 orbit-slot m² certificates. Proof: rewrite kernel and phase to signed radicals and half-integers, then factor √2/8 by ring and cast.
Claim. Let $H$ be a $4\times 4$ real matrix whose fifteen edge-class coefficients equal integers $c_z(d)$, and let $p\in\mathrm{Fin}\,24$ be a coordinate permutation. For any hinge labels $s,t$, the sum over classes $d_0$ of $\mathrm{fullStarClassKernel}(d_0)\cdot c_H(\mathrm{perm}_p(d_0))\cdot(\mathrm{phaseScale}_{\mathrm{symbolDir}}(\mathrm{hingeBase}(s,t),\mathrm{perm}_p(d_0)))^2$ equals $\sqrt{2}/8$ times the integer sum $\sum_{d_0}\mathrm{kernel12Sign}(d_0)\,c_z(\mathrm{perm}_p(d_0))\,(\mathrm{phase2Nat}(s,t,\mathrm{perm}_p(d_0)))^2$.
background
This module closes transported all-orbit $m^2$ moments on the Regge–Bloch 4D stencil by integer (or radical-cancelled) per-orbit certificates. The target identities include $m^2_{\mathrm{transported,all\text{-}orbit}}(\mathrm{axisTTPlus},\mathrm{symbolDir})=-5/2$ and the distinct-hinge weighted moment $-1/4$, with orbit slices on plus fixed as $t_{11}=-3$, $t_{12}=+2$, $t_{13}=-3/2$, and $t_{21}=t_{31}=t_{22}=0$.
The sum here is the kernel push of a Hessian $H$ through the type-12 star kernel. classCoeff extracts the fifteen edge-class components of $H$; permClass p reindexes those classes under a coordinate permutation. phaseScaleDir is the midpoint phase linear in a ray direction; on symbolDir it reduces to the half-integer phase2Nat/2. The cost algebra $H(x)=J(x)+1$ appears only as ambient notation in the import graph, not in the algebraic steps of this lemma.
Upstream, phaseScale_eq_phase2Nat and kernel12_eq_sign supply the exact radical and half-integer normalizations needed to move from real kernel data to an integer certificate.
proof idea
Tactic proof in two layers. First simp_rw applies kernel12_eq_sign, the hypothesis that class coefficients are integer casts, phaseScaleDir_symbolDir, and phaseScale_eq_phase2Nat, so each summand becomes
$(\mathrm{kernel12Sign}(d_0)\cdot\sqrt{2}/2)\cdot c_z(\mathrm{perm}_p d_0)\cdot(\mathrm{phase2Nat}/2)^2$.
A calc block then factors constants: ring on each summand yields the common prefactor $\sqrt{2}/8$, pulled out by Finset.mul_sum. The second step casts the remaining sum to $\mathbb{Z}$ via Int.cast_sum and push_cast, then rings to the stated right-hand side $\sqrt{2}\cdot(\text{integer sum})/8$.
why it matters
Feeds the two orbit-slot certificate theorems m2TransportedOrbitSlotCoeff_t12_eq_cert and m2TransportedOrbitSlotCoeff_t21_eq_cert, which assert that the transported slot coefficients on $t_{12}$ and $t_{21}$ equal the integer certificates $m2OrbitCertZ12$ and $m2OrbitCertZ21$ over 64. Those certificates are the per-orbit bricks that sum to the module's headline moments (plus all-orbit $-5/2$, distinct-hinge $-1/4$, and the matching cross distinct-hinge isotropy).
In the broader Recognition gravity stack this is bookkeeping on the Regge–Bloch 4D Hessian assembly: it converts the real star-kernel push into a form where only integer arithmetic remains, so the orbit slices can be certified without floating radicals. It does not touch continuum isotropy on the bare $e_0$ ray (still open as Regge4DContinuumIsotropyBlockedOnAxisMode) and does not flip gap_action_recovery. Landmarks T7/T8 (eight-tick, $D=3$) set the 4D stencil context but are not invoked here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.