torusSide_pos
plain-language theorem explainer
For every natural number index j, the periodic lattice side length N = j + 3 is strictly positive. Lattice and continuum-limit arguments on the Freudenthal 4-torus cite this to justify denominators, mesh volumes, and N → ∞ indexing. The proof unfolds the definition and closes by elementary arithmetic.
Claim. For every natural number $j$, the periodic-lattice side length $N = j + 3$ satisfies $0 < N$.
background
In the 4D Regge continuum preflight, the side length of the periodic lattice is defined by $N = j + 3$ for $j \in \mathbb{N}$. The continuum family is indexed so the smallest torus already has side at least 3, matching the discrete mesh geometry used for Bloch symbols and Hessian assembly.
This module builds the canonical Recognition mesh on the periodic Freudenthal 4-torus and attaches a value-level exact-$J$ action whose amplitude Hessian is the geometric Option-C midpoint Bloch symbol. Preferred limit shape is amplitude Hessian at fixed mesh, then $N \to \infty$. Positivity of the side length is the elementary arithmetic fact that keeps mesh volumes, normalizations, and continuum indexing well-defined.
Upstream, torusSide is exactly that $j + 3$ definition; no deeper forcing-chain input is required for the inequality itself.
proof idea
One-line tactic proof: unfold the side-length definition to $j + 3$, then omega discharges $0 < j + 3$ over the naturals. No lemmas beyond the definition are used.
why it matters
The Recognition mesh exact-$J$ bridge needs a strictly positive lattice side for every index in the continuum family. Without it, mesh volumes, normalized Hessians, and the $N \to \infty$ Tendsto statements toward the scale-explicit Option-C EH face are ill-typed or vacuous.
This module's campaign goal is the value-level bridge from exact midpoint Bloch symbols to the continuum EH face (RecognitionExactJConvergesEH path), without baking EH into the action and without flipping gap_action_recovery or inhabiting S_RS_converges_EH_4d. The positivity fact is scaffolding arithmetic for that lattice family, not a physics claim. No downstream consumers are recorded yet; it is a local hygiene lemma for the 4-torus mesh carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.