IntMode4
plain-language theorem explainer
Integer-valued wave vectors on the four-torus: maps from a four-point index set into the integers. They label commensurate Bloch modes on the side-N Freudenthal mesh used throughout the Regge 4D continuum preflight. Anyone citing mesh Hessians, exact-J amplitude expansions, or TT-polarized symbols will take this type as the mode argument. The declaration is a pure type abbreviation with no proof content.
Claim. An integer mode in four dimensions is a function $m : \{0,1,2,3\} \to \mathbb{Z}$. Equivalently, $m$ is an integer 4-vector labeling a commensurate Fourier/Bloch mode on the periodic side-$N$ torus via the real covector $k = 2\pi m / N$.
background
The ambient module freezes the independent continuum target for the 4D Regge weak-field campaign before any recovery proof is attempted. The carrier is the canonical periodic Freudenthal 4-torus of side $N \ge 3$, together with Frobenius-normalized Euclidean TT polarizations and an independently defined linearized Einstein-Hilbert quadratic (using the fixed Einstein constant, not a fitted lattice scale).
On that torus the natural discrete momenta are integer lattice vectors. The real wave covector is recovered by the standard scaling $k = 2\pi m / N$. Sibling abbreviations in the same file introduce the companion real mode, wave-norm squared, and momentum-norm identities that convert these integer labels into continuum-looking $|k|^2$ factors.
Nothing in the preflight module claims that the discrete symbol tends to the EH quadratic; those Tendsto propositions remain explicitly open.
proof idea
Pure type abbreviation: IntMode4 is defined to be the function type Fin 4 → ℤ. There is no proof body, no tactic script, and no lemma application. Downstream code simply uses the name as the type of the mode argument.
why it matters
This type is the mode parameter threaded through the entire Recognition-mesh exact-J bridge. Downstream definitions such as exactJActionOnMesh, the amplitude second-difference, and the existence proposition for the exact-J Hessian all take an IntMode4 argument; the value-level identification of that Hessian with the true-weight Regge quadratic is likewise quantified over nonzero integer modes and TT polarizations.
In the broader continuum-closure plan the integer modes are the discrete side of the Bloch symbol that must eventually match the frozen EH coefficient on TT and vanish on pure gauge. The module explicitly keeps continuum Tendsto targets and S_RS_converges_EH_4d uninhabited; the present abbreviation only supplies the carrier type for those later comparisons. It does not itself touch the forcing chain (T0–T8) or the Recognition Composition Law, but it sits inside the gravity-analysis layer that must eventually connect lattice symbols back to the continuum EH target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.