torusSide_ge_three
plain-language theorem explainer
On the canonical periodic Freudenthal 4-torus mesh, the side length N equals j+3 for any natural index j, hence N ≥ 3. Anyone citing the frozen continuum-preflight mesh carrier needs this bound. The proof unfolds the definition and closes by arithmetic.
Claim. For every natural number $j$, the periodic lattice side length $N(j) := j + 3$ satisfies $N(j) \ge 3$.
background
This module is the first binding increment of the 4D continuum closure plan in the QG full-theory campaign. It freezes the independent continuum target, canonical mesh carrier, normalized TT data, pure-gauge family, and honesty decoys before further computation; nothing here proves continuum recovery.
The frozen contracts require a canonical periodic Freudenthal 4-torus mesh of side $N \ge 3$. The side length is defined by torusSide j := j + 3, so the continuum family is indexed by $j \in \mathbb{N}$ with $N = j+3$. That lower bound $N \ge 3$ is the mesh-size floor used throughout the Regge 4D preflight (Frobenius-normalized TT polarizations, exact flat cross-term symbol, and later continuum Tendsto targets).
proof idea
One-line tactic proof: unfold the definition $N(j) = j+3$, then omega discharges $j+3 \ge 3$ for $j : \mathbb{N}$. No external lemmas are required.
why it matters
The module header lists "Canonical periodic Freudenthal 4-torus mesh of side $N \ge 3$" as frozen contract (1). This theorem is the elementary arithmetic witness that the indexed family meets that floor. Downstream continuum and symbol work (exact flat Hessian Bloch symbols, Frobenius pin lemmas, EH quadratic comparison) may assume $N \ge 3$ without re-proving it. It does not itself advance continuum recovery: the OPEN items (Regge4DContinuumEHTarget, S_RS_converges_EH_4d, gapActionRecovery) remain uninhabited. No used-by edges are recorded yet; the lemma is infrastructure for the preflight carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.