rawPhaseQuadratic_normalized
plain-language theorem explainer
Normalizing a nonzero real mode by its Euclidean length multiplies the frozen phase quadratic by the inverse squared norm, bucket by bucket. Continuum-limit arguments for Regge TT moments cite this to pass from raw direction vectors to unit modes without changing the stencil fold shape. The proof unfolds the squared linear phase, clears the positive square root, and finishes by field arithmetic on three coordinates.
Claim. Let $x\in\mathbb{R}^3$ satisfy $\|x\|_2^2>0$, and let $b$ be a bucket. Writing $\hat x:=x/\|x\|_2$, the frozen phase quadratic obeys $Q(\hat x,b)=Q(x,b)/\|x\|_2^2$, where $Q(x,b)=\bigl(\sum_{i=1}^3 x_i\,u_i(b)/2\bigr)^2$ and $u(b)$ is the bucket phase vector.
background
This module is the C-DAG2 continuum stage for Regge TT: after exact Bloch orthogonality removes the cell sum, the remaining work is a local cosine two-jet limit of the finite raw bucket fold. The free-scale theorem keeps phase literally $q\sum_i x_i(u_i/2)$, preserving the doubled-midpoint convention.
A Bucket carries left/right face indices in Fin 6 and a phase vector. The linear phase is the midpoint displacement $\sum_i x_i(u_i/2)$; the frozen phase quadratic is its square. The real-mode squared norm is the Euclidean $\sum_i x_i^2$ on the three spatial components. The moment evaluator folds support with stencil value $-z^2/2$ against a caller-supplied phase quadratic and amplitudes.
Homogeneity under direction normalization is the algebraic bridge that lets later statements replace a raw mode by its unit direction while tracking the exact inverse-norm factor through the fold.
proof idea
From $0<|x|_2^2$ one gets $\sqrt{|x|_2^2}\neq 0$ and $(\sqrt{|x|_2^2})^2=|x|_2^2$. Unfold the quadratic as the square of the linear midpoint phase, expand the three-term Fin 3 sum, then field_simp clears the nonzero square-root denominators. The resulting polynomial identity is discharged by nlinarith. No continuum or Bloch lemma is used; the argument is pure real arithmetic on the phase stencil.
why it matters
Feeds directly into reggeTTMoment_normalized, which lifts the same homogeneity to the full moment evaluator: normalizing the direction multiplies the moment by the expected inverse squared-norm factor against the raw cosine support and bucket amplitudes. That step is required before composing the free-scale cosine two-jet limit with $q_N=2\pi/N$, the eventual finite assembly theorem, and exact momentum-norm normalization in the continuum campaign.
In the gravity analysis stack this is bookkeeping, not a new physical law: it keeps the frozen $x(1/4)$-style phase quadratic consistent when modes are projected to the unit sphere. It does not itself invoke the Recognition forcing chain (T5–T8) or the RCL; it sits downstream in the Regge TT continuum certificate path.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.