freudenthalBoundedComplex_nV
plain-language theorem explainer
The side-$N$ periodic Freudenthal torus, packaged as a bounded complex for path-sum probes, has vertex count exactly $N^3$. Discrete-gravity and census workers cite this when matching torus embeddings to path-sum state-space observables. The proof is a one-line term application of the grid vertex-cardinality fact.
Claim. For every positive integer $N$, the vertex-count field of the bounded complex obtained by embedding the side-$N$ periodic Freudenthal torus equals $N^3$.
background
Module lane is Seven Gaps Phase 2b path-sum probes C3 and C6. It is probe-only: it attaches the canonical periodic Freudenthal torus (from the periodic-torus geometry module) to the scoped path-sum state space BoundedComplex, and records honest count and automorphism facts without claiming measures, limits, or continuum behavior.
Probe C3 packages the side-$N$ torus ($N \ge 1$) as an element of that bounded-complex type with edge budget $7N^3$. The vertex, edge, and tetrahedron counts are required to match the canonical periodic triangulation: vertices $N^3$, edges $7N^3$, tets $6N^3$. The field nV is the vertex-count observable on census/ensemble data in the Seven Gaps gravity stack.
Upstream, the sibling card_vertex supplies the raw count of vertices of the $N\times N\times N$ periodic grid (equivalently $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$). The present theorem simply identifies the bounded-complex vertex field with that count.
proof idea
One-line term proof: the goal is definitionally the statement of card_vertex N, so the proof is just that lemma applied at $N$. No further rewriting or case analysis.
why it matters
Closes the vertex half of the C3 provenance record: the embedded torus really does carry $nV = N^3$, as required for the diagonal embedding into the path-sum state space. Together with the companion edge and tet count theorems it underwrites the claim that the packaging preserves the three census counts of the canonical periodic triangulation, and feeds the later match-to-canonical identity.
In the broader Recognition gravity program this is bookkeeping for discrete path-sum probes on the eight-tick / $D=3$ lattice geometry, not a dynamical or continuum result. No downstream consumers are wired yet in the graph; the lemma exists so later Aut-cardinality and measure upper-bound probes (C6 branch) can quote a pinned vertex count when bounding $\mu(T_N)\le 1/N^3$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.