rawPhaseLinear
plain-language theorem explainer
Literal midpoint-displacement phase for a Regge TT bucket: sum of three mode components times half the integer phase components. Downstream continuum cosine two-jet work cites it as the linear kernel of the free-scale phase q·Σ x_i(u_i/2). The body is a direct three-term sum encoding the doubled-midpoint convention.
Claim. For a real mode direction $x:\{0,1,2\}\to\mathbb{R}$ and a bucket with integer phase vector $u$, the raw linear phase is $\sum_{i=0}^{2} x_i\cdot(u_i/2)$.
background
This module is the C-DAG2 continuum stage for Regge TT cosine two-jet limits. Exact Bloch orthogonality has already removed the cell sum, so the remaining analysis is a local cosine two-jet of the finite raw bucket fold. The free-scale phase is literally $q\sum_i x_i(u_i/2)$, preserving the doubled-midpoint convention; the constant term is killed by the assembled zero-mode theorem.
A bucket carries left/right face indices in $\mathrm{Fin},6$ and a three-component phase vector $u$. The components $u_i$ are the integer displacements along the three spatial directions. Dividing by two is the doubled-key (midpoint) normalization used throughout the assembly and the continuum bridge.
Related phase notions elsewhere (eight-tick $k\pi/4$, continuum plane-wave $k\cdot x$) are not used here; this definition is the discrete bucket midpoint phase only.
proof idea
Pure definition, no proof. Expand as the finite sum $\sum_{i:\mathrm{Fin},3} x_i\cdot((u_i:\mathbb{Z}):\mathbb{R})/2$ with integer-to-real coercion on the bucket phase components. The factor $1/2$ is baked into the summand rather than applied outside.
why it matters
Linear kernel of the C-DAG2 continuum stage. It is squared to form the frozen phase quadratic, and fed to the free-scale cosine evaluator $\cos(q\cdot\mathrm{rawPhaseLinear})$. The reusable headline rawCosineFold_scale_tendsto then shows that, after assembled zero-mode cancellation, the raw cosine fold divided by $q^2$ tends to the Regge TT moment built from this literal midpoint phase quadratic.
Also identifies the commensurate lattice evaluator at $q_N=2\pi/N$ with the free-scale form, and supports the normalized quadratic identity (direction divided by its Euclidean norm). The doubled-midpoint convention is thereby preserved from the finite Bloch assembly all the way into the continuum two-jet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.