freudenthalBoundedComplex_nT
plain-language theorem explainer
On the path-sum embedding of the side-N periodic Freudenthal torus, the tetrahedron count equals 6 N^3. Anyone citing the C3 diagonal embedding or non-emptiness of that complex needs this identity. The proof is a one-line appeal to the finite-cardinality count of the periodic tetrahedron type.
Claim. For every positive integer $N$, the tetrahedron count of the bounded complex obtained by embedding the side-$N$ periodic Freudenthal torus equals $6 N^3$.
background
Module PathSumProbes is a non-flag-bearing probe lane. It attaches the canonical periodic Freudenthal torus to the scoped path-sum state space BoundedComplex and records only cheap combinatorial facts (counts and incidence maps), with no claims about measures, limits, or continuum behavior.
The embedding freudenthalBoundedComplex N (Probe C3) packages the side-$N$ torus as an element of BoundedComplex (7 N^3). Its fields nV, nE, nT are defined as the finite cardinalities of the vertex, periodic-edge, and periodic-tetrahedron types of the canonical triangulation. The module docstring preserves the count triple $nV = N^3$, $nE = 7 N^3$, $nT = 6 N^3$ as definitional inheritance from that triangulation.
Upstream, card_periodicTet already proves that the periodic tetrahedron set at side $N$ has cardinality $6 N^3$, via the product identification with vertices times Fin 6.
proof idea
One-line term proof: the nT field of the embedded complex is definitionally Fintype.card (PeriodicTet N N N), so the claim is exactly card_periodicTet N. That lemma reduces the count to card(Vertex × Fin 6) = 6 N^3 by product cardinality, the vertex-count identity, and card(Fin 6) = 6.
why it matters
This is one of the three preserved count identities for Probe C3. Downstream, freudenthalBoundedComplex_nT_pos rewrites through it and uses NeZero N to conclude the embedded torus is non-empty (has tetrahedra), blocking the empty-configuration landmine before Aut and measure bounds are discussed.
In the Seven Gaps gravity lane this sits under path-sum probes only: it feeds the provenance record that the Freudenthal torus really lands inside the BoundedComplex state space with the expected tet count, without touching continuum path sums or any Recognition forcing step (T0–T8). It closes no open scaffold; it is already proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.