phaseScale_eq_phase2Nat
plain-language theorem explainer
Along the (1,1,0,0) symbol direction, the continuous phase scale of a hinge base plus half-class displacement equals half an explicit integer phase built from the two active mask bits and two class bits. Anyone computing the (1,1)-orbit m² slot coefficient cites this identity to replace real arithmetic by a certified Nat formula. The proof is pure case analysis on four Boolean bits after unfolding the sums.
Claim. For every hinge index $s\in\{0,\ldots,23\}$, triangle index $t\in\{0,\ldots,9\}$, and class index $d\in\{0,\ldots,14\}$, the phase scale of the hinge base point against class displacement $d$ equals $\mathrm{phase2Nat}(s,t,d)/2$ as a real number. Explicitly, if $x$ is the $\{0,1\}^4$ coordinate mask of the hinge and $v$ is the class displacement, then $\sum_i e_i x_i + \tfrac12\sum_i e_i v_i = n/2$ where $e=(1,1,0,0)$ and $n\in\mathbb{N}$ is the integer phase built from the two active mask bits and the two class bits of $d$.
background
This module isolates the (1,1)-orbit contribution to the small-momentum ($m^2$) symbol of the 4D Regge Bloch fold blochFold11. It never redefines Hessians, kernels, or stencils; it only evaluates folds along the fixed direction symbolDir = (1,1,0,0).
The continuous phase scale of a 4-vector $x$ against a class $d$ is
$\mathrm{phaseScale}(x,d)=\sum_i e_i x_i+\tfrac12\sum_i e_i(\mathrm{classDisp},d)_i$
with $e=(1,1,0,0)$. The hinge base is the ${0,1}$-coordinate mask of the triangle vertex mask: each coordinate is $1$ iff the corresponding bit of the mask is set. The integer companion phase2Nat packs the same data as
$2\cdot(\mathrm{bit}_0+\mathrm{bit}_1)+\mathrm{classBit}_0+\mathrm{classBit}_1$,
so that dividing by $2$ recovers the real phase.
Only the first two coordinates of $e$ are nonzero, so both sums collapse to those two axes. The class-bit and mask-bit predicates come from the edge-stencil and fold modules imported here.
proof idea
Term-mode proof by exhaustive Boolean case split. Unfold phaseScale, phase2Nat, hingeBase, maskCoord, classDisp, and symbolDir. The four-term Fin sums reduce via Fin.sum_univ_four to the two active axes of $e=(1,1,0,0)$. Nested by_cases on the two mask bits of the triangle vertex mask and the two class bits of $d$ produces sixteen leaves; each leaf is discharged by simp on the bit hypotheses followed by ring. No external lemmas beyond the unfolded definitions are required.
why it matters
This identity is the bridge from the continuous $m^2$ phase to a fully integer certificate. Downstream, m2SlotCoeff_eq_cert uses it to prove that the real slot coefficient equals a certified integer expression divided by $32$. The same equality is invoked in the transported-orbit evaluations ker_push_sqrt2_half, ker_push_sqrt3, and m2TransportedOrbitSlotCoeff_t22_eq_cert, which push class kernels through permutations while keeping coefficients exact.
In the module's landed list it supports the closed-form claim that the $m^2$ symbol equals $-3$ on the nonzero TT sector and $0$ on gauge. It does not close the open Prop FoldAlongM2Tendsto (punctured Tendsto glue of fold over $\mu^2$), nor the global Einstein-Hilbert recovery goals flagged in the module doc. Within Recognition gravity analysis it is local scaffolding for the (1,1) orbit only; the eight-tick and $D=3$ forcing chain are upstream background, not direct inputs here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.