freudenthalBoundedComplex_nE
plain-language theorem explainer
For every positive integer N, the edge count of the BoundedComplex built from the side-N periodic Freudenthal torus equals exactly 7 N^3, saturating the census cap. Discrete-gravity and Seven Gaps workers cite this when wiring the canonical torus into the path-sum state space. The proof is a one-line appeal to the periodic-edge cardinality lemma.
Claim. For every natural number $N \ge 1$, the edge-count field of the bounded complex obtained by embedding the side-$N$ periodic Freudenthal 3-torus equals $7 N^{3}$.
background
The module is Seven Gaps Phase 2b, lane O: path-sum probes C3 and C6. It is explicitly non-flag-bearing. It records cheap attachment facts between the canonical periodic Freudenthal torus and the scoped path-sum type BoundedComplex, and makes no claim about measures, limits, or continuum behavior.
A BoundedComplex packages vertex/edge/tetrahedron counts plus incidence maps for edges and tets. The construction at side $N$ (any $N \ge 1$) embeds the periodic triangulation of the 3-torus into that state space with edge budget fixed at the census cap $7 N^{3}$. Companion census data are $nV = N^{3}$ and $nT = 6 N^{3}$.
Upstream, the periodic-edge cardinality lemma shows that the set of edges of the $N \times N \times N$ Freudenthal torus has size $7 N^{3}$ (seven edge directions per cell). The edge-count observable on ensembles is the corresponding real-valued census field.
proof idea
One-line term proof. The edge-count field of the embedded complex is definitionally the periodic-edge cardinality, so the equality is exactly the already-proved lemma that the periodic edge set on the side-$N$ torus has cardinality $7 N^{3}$.
why it matters
Closes the edge half of PROBE C3's preserved census triple for the diagonal embedding of the periodic Freudenthal torus into the path-sum state space. The module doc states the cap is met exactly: $nE = 7 N^{3}$, together with $nV = N^{3}$ and $nT = 6 N^{3}$, all definitionally matching the canonical periodic triangulation fields.
No downstream consumers are recorded yet. The result is a provenance and landmine-check fact, not a continuum or measure theorem. Sibling count lemmas finish the census; the matching lemma ties the package back to the geometry module. In the RS gravity stack this keeps discrete 3-geometry honest (framework landmark T8: $D = 3$) before any later path-sum or automorphism analysis (PROBE C6) is attempted.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.