freudenthalBoundedComplex_edgeVerts
plain-language theorem explainer
Edge-endpoint incidence on the bounded-complex packaging of the side-$N$ periodic Freudenthal torus equals the canonical $N\times N\times N$ encoder map. Probe authors cite it when attaching the torus to the path-sum state space without changing incidence. The equality is definitional: a one-line reflexivity proof.
Claim. For every positive integer $N$, the edge-endpoint incidence map of the bounded complex that packages the side-$N$ periodic Freudenthal torus equals the canonical edge-vertex incidence map of 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 on measures, continuum limits, or path-sum values. Probe C3 packages the canonical periodic Freudenthal torus of side $N\ge 1$ as an element of the scoped path-sum type BoundedComplex with capacity $7N^3$.
That packaging is required to preserve vertex/edge/tet counts and the two incidence maps (edge endpoints and tet corners), each definitionally equal to the corresponding field of the canonical periodic triangulation on $N\times N\times N$. The edge-endpoint map records, for each edge index, the ordered pair of vertices it joins; the canonical encoder supplies the reference implementation on the Freudenthal cube triangulation of the discrete 3-torus.
BoundedComplex deliberately drops edge-in-tet assignment and per-tet metric data, so only the incidence maps that fit the scoped class are retained. This lemma is the edge half of that retention record.
proof idea
Term-mode one-liner: rfl. The bounded-complex constructor sets its edge-endpoint field to the canonical encoder map on side $(N,N,N)$, so the two sides are definitionally equal and no lemma application is needed.
why it matters
Closes the edge-incidence half of PROBE C3's preservation list: when the periodic Freudenthal torus is attached to the path-sum state space, edge endpoints are not reinvented. Together with the matching tet-corner and count lemmas, it underwrites the sibling statement that the packaged complex matches the canonical periodic triangulation on all fields the scoped class can carry.
No downstream consumers are recorded yet; the lemma is provenance infrastructure for later path-sum work on the torus image. It does not touch forcing-chain landmarks (T5–T8), RCL, or constants; it only keeps discrete incidence honest inside the gravity seven-gaps probe lane. Simpliciality of the image and any measure or continuum claim remain explicitly out of scope.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.