torusSide
plain-language theorem explainer
Defines the side length of the canonical periodic 4-torus mesh as N = j + 3 for continuum index j. Anyone citing the Freudenthal mesh family, continuum Tendsto targets, or Recognition exact-J bridges uses this indexing. The body is the one-line arithmetic shift that enforces N ≥ 3.
Claim. For each continuum index $j \in \mathbb{N}$, the side length of the periodic lattice is $N = j + 3$.
background
The module freezes the independent continuum target and canonical mesh carrier for the 4D Regge weak-field campaign before any continuum recovery is proved. The frozen contract requires a canonical periodic Freudenthal triangulation of the flat 4-torus with side $N \ge 3$.
The continuum family is indexed by a natural number $j$; this definition converts that index into the geometric side length. Downstream mesh structures (CanonicalFreudenthalTorus4D, RecognitionFreudenthalMesh4D) store only the continuum index and recover the side via this map. The shift by three is the bookkeeping that keeps every mesh in the admissible range without a separate positivity hypothesis at every call site.
proof idea
Pure definition: the body is the arithmetic expression $j + 3$. No lemmas, tactics, or hypotheses.
why it matters
This is the single naming of the continuum-family side length used across the preflight and the Recognition mesh bridge. CanonicalFreudenthalTorus4D.side and RecognitionFreudenthalMesh4D.side both reduce to it. Continuum Props such as RecognitionExactJConvergesEH and RecognitionExactJConvergesGaugeZero quantify over mesh side via the same index, sending $N \to \infty$ after $|k|^2$ normalization toward the frozen Einstein-Hilbert quadratic face. The positivity lemma torusSide_pos and the geometric carrier constructions hang off this one-line shift. It does not itself close continuum recovery; the module marks those Tendsto Props OPEN.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.