card_periodicTet
plain-language theorem explainer
The set of periodic tetrahedra on the side-$N$ cubic torus has cardinality $6N^3$. Gravity path-sum work cites this when packaging the canonical Freudenthal torus into a BoundedComplex (PROBE C3). The proof is a short product-cardinality calculation once tetrahedra are identified with vertices times six orientations.
Claim. For every natural number $N$, the finite set of periodic tetrahedra on the $N\times N\times N$ torus has cardinality $6N^3$.
background
Module PathSumProbes is a non-flag-bearing provenance lane: it records cheap honest facts linking the canonical periodic Freudenthal torus to the scoped path-sum configuration class BoundedComplex, and claims nothing about measures, limits, or continuum behavior.
Vertices of the side-$N$ torus are the product grid $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$, with cardinality $N^3$ (sibling card_vertex). Periodic tetrahedra are the discrete tet cells of the Freudenthal triangulation of that torus; combinatorially they amount to a choice of base vertex together with one of six oriented tet types, i.e. a product with $\mathrm{Fin},6$.
PROBE C3 packages the torus at cap $B=7N^3$ with preserved counts $nV=N^3$, $nE=7N^3$, $nT=6N^3$ and the two incidence maps edgeVerts and tetVerts, while dropping edge-in-tet slots and per-tet metrics.
proof idea
PeriodicTet $N,N,N$ is definitionally the product Vertex $N,N,N\times\mathrm{Fin},6$. The proof therefore reduces the goal to $\lvert V\times\mathrm{Fin},6\rvert=6N^3$. Rewrite by Fintype.card_prod, apply card_vertex (so $\lvert V\rvert=N^3$) and Fintype.card_fin (so $\lvert\mathrm{Fin},6\rvert=6$), then close by ring. No geometric content is used beyond that product presentation.
why it matters
This count is the tetrahedron field of freudenthalBoundedComplex: that definition sets nT to Fintype.card (PeriodicTet $N,N,N$), and freudenthalBoundedComplex_nT is the one-line specialization $(T_N).nT=6N^3$ obtained by applying this theorem. Together with the matching vertex and edge counts it pins the diagonal embedding of the Freudenthal torus into BoundedComplex$(7N^3)$ as PROBE C3 in the Seven Gaps path-sum lane.
The module is explicit that this is provenance framing only: no path-sum value, no continuum limit, and no IsSimplicial claim. Downstream Aut-vacuity checks (PROBE C6) use the embedded complex, not this cardinality lemma directly, but they inherit a correctly sized tet set from it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.