axisIntMode
plain-language theorem explainer
Defines the integer four-mode (1,0,0,0) on the torus, the axis wave used by plus and cross TT witnesses. Anyone checking continuum-symbol agreement or EH matching on a fixed direction cites this constant mode. The body is a one-line Fin 4 map sending the zeroth slot to 1 and the rest to 0.
Claim. Let $\mathrm{IntMode}_4 := \mathrm{Fin}\,4 \to \mathbb{Z}$ be the space of integer wave vectors on the side-$N$ four-torus. The axis integer mode is the map $m:\mathrm{Fin}\,4\to\mathbb{Z}$ with $m(0)=1$ and $m(i)=0$ for $i\neq 0$, i.e. the commensurate mode $(1,0,0,0)$.
background
This module is the 4D Regge algebraic closer: it banks available identities (decoy one-orbit mismatch, plus/cross TT witnesses, gauge vanishing, full zero-momentum moments) and names full TT isotropy, pure-gauge vanishing, and plus-cross agreement as OPEN Props with status false. It does not claim $S_{RS}$ converges to Einstein-Hilbert in 4D.
IntMode4 is the type of integer wave vectors on the side-$N$ torus (commensurate modes); the real covector is $k=2\pi m/N$. The frozen continuum target coefficient is einsteinHilbertTTCoefficient4D $= -1/4$, fixed independently of the lattice so the closer must observe the match rather than rescale to it.
Plus and cross Frobenius-normalized TT polarizations are the banked witnesses against which continuum symbols are evaluated. The axis mode supplies a single nonzero integer direction on which those witnesses are compared.
proof idea
Pure definitional construction: a function on Fin 4 that returns the integer 1 at index 0 and 0 elsewhere. No lemmas, tactics, or upstream theorems are applied; the term is the axis mode $(1,0,0,0)$ as an IntMode4.
why it matters
Feeds the OPEN target Regge4DPlusCrossAgreeTarget, which asserts that for this axis mode the concrete transported continuum symbols of the plus and cross normalized TT polarizations agree (both should eventually equal the frozen EH coefficient $-1/4$). Without a fixed nonzero integer direction, plus-cross agreement and the full TT isotropy campaign have no concrete test vector.
In the QG full-theory stack this is the 4D counterpart of the 3D algebraic closer's axis setup: bank the mode, bank the polarizations, then demand that geometry-derived symbols hit the preflight EH coefficient. It does not flip gap action recovery or prove continuum convergence; it only pins the mode used by those named OPEN Props.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.