freudenthalBoundedComplex_nT_pos
plain-language theorem explainer
For every positive integer side length N, the periodic Freudenthal torus packaged as a bounded complex has a strictly positive tetrahedron count. Anyone citing the non-empty path-sum state space for probe C3 needs this positivity. The proof rewrites the count as 6 N^3 and closes by elementary positivity of powers.
Claim. For every natural number $N \ge 1$, if $T_N$ is the bounded complex obtained by embedding the canonical periodic Freudenthal torus of side $N$, then the number of tetrahedra satisfies $n_T(T_N) > 0$.
background
Module PathSumProbes records two cheap provenance facts (probes C3 and C6) linking the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex. It makes no continuum, measure, or limit claims.
Probe C3 packages the torus of side $N \ge 1$ as freudenthalBoundedComplex N inside BoundedComplex (7 N^3). Preserved counts are $n_V = N^3$, $n_E = 7 N^3$, $n_T = 6 N^3$, together with edge-endpoint and tet-corner incidence maps, all definitionally matching canonicalPeriodicTriangulation N N N. Dropped fields include edge-in-tet assignment and per-tet metric data.
The sibling identity freudenthalBoundedComplex_nT supplies the exact formula $n_T = 6 N^3$ used here. The present lemma is the non-vacuity half of that count: the embedded configuration is not an empty complex.
proof idea
One short tactic proof. Rewrite the tetrahedron count via the sibling lemma freudenthalBoundedComplex_nT, obtaining the goal $0 < 6 N^3$. From the instance NeZero N extract $0 < N$, lift to $0 < N^3$ by pow_pos, and finish with omega (which absorbs the constant factor 6).
why it matters
Non-vacuity of the tetrahedron set is the minimal geometric sanity check before any path-sum or automorphism argument on the embedded torus can be stated. The module frames this under probe C3: attach the Freudenthal torus to the path-sum state space while preserving vertex/edge/tet counts and incidence maps.
Downstream the same complex supports the translation-automorphism embedding (probe C6): the group $\mathbb{Z}_N^3$ injects into Aut(T_N), yielding $|\mathrm{Aut}(T_N)| \ge N^3$ and the measure bound $\mu(T_N) \le 1/N^3$. Without $n_T > 0$ those statements would sit on an empty configuration.
In the broader Recognition gravity lane this is scaffolding hygiene, not a forcing-chain step (T0–T8). It closes a landmine that the periodic triangulation could collapse to zero tets under the BoundedComplex packaging. No parent theorem currently depends on it in the graph; it is a local non-emptiness certificate for the Seven Gaps path-sum probes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.