freudenthalExplicitFiberPairSelectedCell
plain-language theorem explainer
For a typed positive-displacement periodic edge on the cubic torus and a local Freudenthal (tetrahedron, edge-slot) pair, returns the unique periodic cell selected by the explicit fiber entry. Discrete-gravity and Regge-lattice proofs cite it when aligning six-tet local data with global periodic edges. The body is a direct call to the periodic base-cell matcher on the cube-edge base of the pair's local edge and the edge base.
Claim. Let $N_x,N_y,N_z\ge 1$. Given a positive-displacement periodic edge $e$ on the $N_x\times N_y\times N_z$ cubic torus (base vertex plus one of seven cube displacements) and a local Freudenthal pair $(\tau,s)\in\{0,\ldots,5\}^2$ (tetrahedron index and edge slot), return the unique periodic vertex (cell) obtained by matching the cube-edge base of the global edge representative of $(\tau,s)$ against the base of $e$.
background
This module packages the exact theorem obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it wires the encoded periodic scaffold to the model target.
A local Freudenthal pair is an element of $\mathrm{Fin},6\times\mathrm{Fin},6$: tetrahedron index together with an edge slot in the six-tet cubic triangulation. Periodic vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A periodic edge is a base vertex plus a positive cube displacement in $\mathrm{Fin},7$. Upstream, the cube triangulation's local-edge map sends each (tet, slot) to one of 19 one-cube edge representatives; cube-edge base then sends that representative to a local cube vertex in $\mathrm{Fin},8$. The torus local-edge map translates those data by a cell offset into a full periodic edge.
The body uses the periodic matching base-cell operation that isolates the unique cell whose base offset reconciles a local cube-edge base with a typed edge base.
proof idea
Definitional one-liner, not a tactic proof. From the local pair $(\tau,s)$, apply the cube triangulation local-edge map to obtain a $\mathrm{Fin},19$ edge index; take that index's cube-edge base in $\mathrm{Fin},8$; feed the result together with the typed periodic edge's base vertex into the periodic matching base-cell map, which returns the selected torus vertex. No further rewriting or uniqueness argument appears in the definition itself.
why it matters
This cell selector is the explicit fiber bridge used throughout the physical six-tet Dirichlet instance. Downstream, the five-period specialization is proved equal to it by unfolding both sides and invoking uniqueness of the matching base cell; the axis-witness selected-cell identity likewise reduces to that uniqueness on the displacement-0 fiber. It is threaded into the expanded length-chain and angle-chain forms of the canonical periodic mixed hinge-deficit targets, and into equating local-pair expanded inner sums with slot-guarded sums.
Those targets are the exact obligations that connect the encoded periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model. In the RS gravity stack this sits on the Regge/cubic-lattice path toward a continuum Dirichlet action, not on the T0–T8 forcing chain. Callers that need uniqueness cite the matching-base-cell uniqueness lemma separately.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.