instNeZeroAddThree
plain-language theorem explainer
For every natural number j, the integer j+3 is nonzero. Analysts of the Regge TT continuum limit cite this whenever finite tori are indexed by side length N = j+3 (so N ≥ 3). The proof is a one-line omega discharge of the NeZero instance obligation.
Claim. For every natural number $j$, one has $j+3 \neq 0$ (as a natural number).
background
The module sets up Stage 1 of the Regge TT continuum-symbol program: the true nonlinear 3D Regge action on the canonical periodic Freudenthal torus, its flat point, and the TT Bloch symbol object. Finite tori are parameterized by a side length $N$, and the continuum limit is taken along the sequence $N = j+3$ for $j \in \mathbb{N}$, so that $N \ge 3$ and the commensurate momenta $k_N = 2\pi \cdot m/N$ shrink to zero at fixed direction.
Many of the finite-lattice constructions (periodic edge fields, canonical reduced symbols, momentum-norm squares) are typed over a parameter $N : \mathbb{N}$ that must satisfy NeZero N, because the torus, the plane-wave phases, and the normalizations divide by $N$. Supplying NeZero (j+3) once, as an instance, lets every downstream call at side $j+3$ resolve that obligation automatically.
proof idea
Instance constructor: the NeZero witness is the proposition $j+3 \neq 0$, discharged by the omega tactic on natural-number arithmetic. No lemmas are invoked; there is no algebraic content beyond $j+3 \ge 3$.
why it matters
Without this instance, every continuum-limit statement that indexes the finite reduced Regge TT symbol at $N = j+3$ would need an inline nonzero proof. It is applied explicitly in the three closers that finish the program: canonicalFiniteH_div_momentumNormSq_tendsto (P1.1a headline convergence of the normalized finite symbol), canonicalFiniteH_div_momentumNormSq_tendsto_isotropy (P1.1a+b composed isotropy to exactly $-1/4$), and reggeTTContinuumIsotropyTarget_closed (the verbatim 3D closer that discharges the open target ReggeTTContinuumIsotropyTarget). Those theorems supersede the C10 numerical evidence that the continuum TT Bloch symbol is isotropic with the linearized Einstein-Hilbert coefficient $-1/4$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.