freudenthalBoundedComplex_matches_canonical
plain-language theorem explainer
All five shared incidence fields of the bounded-complex packaging of the side-N Freudenthal torus agree definitionally with the canonical periodic triangulation on the N×N×N torus. Path-sum and gravity authors cite this as the PROBE C3 provenance record attaching that torus to the BoundedComplex state space. The proof is five reflexivity steps: the packaging is a field-wise copy by construction.
Claim. For every positive integer $N$, writing $T_N$ for the bounded-complex packaging of the side-$N$ periodic Freudenthal torus and $C_N$ for the canonical periodic triangulation of the $N\times N\times N$ torus, one has $n_V(T_N)=n_V(C_N)$, $n_E(T_N)=n_E(C_N)$, $n_T(T_N)=n_T(C_N)$, and the edge-endpoint and tetrahedron-corner incidence maps of $T_N$ equal those of $C_N$.
background
The ambient module is a non-flag-bearing probe lane: it records cheap honest facts linking the canonical periodic Freudenthal 3-torus to the scoped path-sum state space BoundedComplex, and claims nothing about measures, limits, or continuum behavior.
The Freudenthal cube triangulation of the 3-torus of side $N$ supplies a periodic simplicial complex whose vertices are $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$ (so $n_V=N^3$), with $n_E=7N^3$ positive-displacement edges and $n_T=6N^3$ tetrahedra. The packaging freudenthalBoundedComplex N embeds that complex into BoundedComplex at capacity $7N^3$, retaining only the five fields that both shapes share: counts $n_V,n_E,n_T$ and the incidence maps sending each edge (resp. tet) to its endpoint (resp. corner) vertices.
BoundedComplex deliberately drops the edge-slot-in-tetrahedron assignment and any per-tet metric; the scoped class is equilateral-at-fixed-scale by model convention. Neither shape carries a 2-face list. The present theorem is the definitional comparison that makes the packaging honest.
proof idea
Pure term-mode definitional equality. The packaging is constructed so that each of the five fields is definitionally the corresponding field of canonicalPeriodicTriangulation N N N. The proof is therefore the five-component pair of rfl proofs; no lemmas are invoked and no rewriting is required.
why it matters
This is the PROBE C3 provenance record in the Seven Gaps Phase 2b path-sum lane. It attaches the canonical periodic Freudenthal torus (the natural $D=3$ periodic complex forced by the T8 dimension step and the eight-tick octave geometry) to the path-sum state space without smuggling measure or continuum claims.
Downstream the module uses the same packaging for PROBE C6: the translation group $\mathbb{Z}_N^3$ embeds into the relabeling automorphisms of the image, yielding $|\mathrm{Aut}(T_N)|\ge N^3$ and the crude measure bound $\mu(T_N)\le 1/N^3$. No external parent theorem currently depends on this comparison (used-by is empty); its role is local honesty of the embedding.
What remains open in the same lane is simpliciality of the image and any continuum or path-sum evaluation; those are explicitly not claimed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.