freudenthalBoundedComplex_tetVerts
plain-language theorem explainer
For every positive integer N, the tetrahedron-corner incidence map on the Freudenthal bounded complex of side N equals the canonical tet-vertex encoder on the N×N×N periodic triangulation. Path-sum and discrete-gravity workers cite this as provenance that packaging the torus into BoundedComplex preserves tet incidence. The proof is pure definitional equality (rfl).
Claim. For every positive integer $N$, if $T_N$ is the bounded complex obtained by packaging the side-$N$ periodic Freudenthal torus into the path-sum state space, then the tetrahedron-corner incidence of $T_N$ equals the canonical tetrahedron-vertex assignment on the $N\times N\times N$ periodic triangulation.
background
Module lane is Seven Gaps Phase 2b, path-sum probes C3 and C6. Status is probes only: no claim about measures, continuum limits, or path-sum values. Probe C3 attaches the canonical periodic Freudenthal torus at side $N\ge 1$ as an element of the scoped path-sum type BoundedComplex with edge budget $7N^3$.
That packaging is required to preserve three incidence-shape fields definitionally: vertex/edge/tet counts, edge-endpoint incidence, and tetrahedron-corner incidence. The last of these is the map sending each tetrahedron index to its four corner vertices on the $N^3$ lattice torus. The canonical encoder is the corresponding field of the periodic Freudenthal triangulation at equal side lengths $(N,N,N)$.
What is dropped by design: the edge-slot-in-tet assignment and any per-tet metric. The scoped complex is equilateral-at-fixed-scale by model convention and carries no 2-face list. Simpliciality of the image is not claimed here.
proof idea
Term-mode one-liner: rfl. By construction of the packaging map, the tet-corner field of the bounded complex is definitionally the canonical tet-vertex encoder at side triple $(N,N,N)$. No lemma application or rewriting is required beyond that definitional match; the [NeZero N] instance only ensures the side is admissible for the periodic torus.
why it matters
Closes one of the five shared incidence fields in the Probe C3 provenance record: counts, edge endpoints, and tet corners must all agree definitionally with the canonical periodic triangulation so that later path-sum work can treat the packaged torus as the same combinatorial object, not a silent re-encoding.
Sibling equalities cover nV, nE, nT, and edge endpoints; the matching bundle theorem records that all five agree at once. Downstream Aut-vacuity checks (Probe C6) and any future measure bounds sit on this attachment, but this declaration itself has no recorded dependents yet.
Framework role is infrastructural inside discrete gravity on the Freudenthal lattice, not a forcing-chain (T0–T8) step. It does not touch J-cost, phi-ladder masses, or the alpha band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.