freudenthalBoundedComplex
plain-language theorem explainer
The canonical periodic Freudenthal torus of side N is packaged as a bounded complex with capacity 7 N³. Path-sum and class-mass arguments in the Seven Gaps gravity lane cite this embedding to place the torus inside the scoped state space. The body is a structure instance: counts and incidence maps come from the canonical periodic triangulation, and the three budget inequalities are discharged by elementary cardinality lemmas.
Claim. For every positive integer $N$, the periodic Freudenthal triangulation of the $N\times N\times N$ torus is realized as a bounded complex of capacity $B=7N^3$, with vertex count $N^3$, edge count $7N^3$, tetrahedron count $6N^3$, and incidence maps equal to the canonical edge-endpoint and tetrahedron-corner maps of that triangulation.
background
Lane O of Seven Gaps Phase 2b records path-sum probes only. It makes no claim about measures, continuum limits, or the value of any path sum. The scoped state space is BoundedComplex B: a finite 3-complex whose vertex, edge, and tetrahedron counts are each at most the budget $B$, together with incidence maps sending edges to endpoint pairs and tets to corner 4-tuples.
The geometric source is the canonical periodic Freudenthal triangulation of the discrete 3-torus of side $N$ (vertices $\mathrm{Fin},N^3$, edges and tets from the standard cube triangulation, periodized). Its counts are $n_V=N^3$, $n_E=7N^3$, $n_T=6N^3$. Choosing $B=7N^3$ therefore fits the complex inside the budget with room only on the tet side.
PROBE C3 is the diagonal embedding of that torus into the path-sum state space. Incidence shape is deliberately incomplete: BoundedComplex has no edge-in-tet slot field and no per-tet metric, so those data from the full triangulation are dropped and recorded as such in the module status.
proof idea
Structure instance, not a deep proof. Vertex, edge, and tet counts are the Fintype.card of the corresponding periodic types. The vertex budget $N^3\le 7N^3$ rewrites via the vertex-count lemma, then $N^3=1\cdot N^3\le 7N^3$ by one_mul and Nat.mul_le_mul. The edge budget is equality to the periodic-edge card lemma. The tet budget is $6N^3\le 7N^3$ after the periodic-tet card lemma. Incidence maps are definitionally the canonical edge-endpoint and tet-corner maps of the periodic triangulation.
why it matters
This is the attachment point that lets the Freudenthal torus sit inside path-sum bookkeeping. Downstream class-mass theorems in FreudenthalTorusClassMass quantify over complexes equivalent (under relabeling) to this embedding: each labeled torus representative has symmetry-factor mass $\mu\le N^{-3}$; labeled summands $\mu\cdot z$ with $|z|\le 1$ are likewise bounded; both $\mu(T_{N+1})$ and the labeled summand sequence tend to 0 at infinity. Class mass is identified as fiber cardinality times $\mu$, and bounded by $|\mathrm{fiber}|/N^3$ without claiming absolute $N^{-3}$ suppression of the pushforward.
In-module, the same object feeds the Aut-vacuity landmine check (PROBE C6): translations embed into the relabeling automorphism group, giving $|\mathrm{Aut}|\ge N^3$ and the $\mu\le N^{-3}$ bound. Framework role is scaffolding for honest gravity path-sum estimates on the discrete 3-torus, not a continuum or measure claim. Simpliciality of the image is explicitly not proved here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.