periodicMatchingBaseCell_spec
plain-language theorem explainer
On a periodic cubic lattice, every target vertex is recovered by adding a fixed 3-bit offset (indexed by Fin 8) to a uniquely chosen base cell. Lattice gravity and Regge-action constructions cite this to pin the matching cell that carries a local Freudenthal edge. The proof is the first projection of the Classical.choose specification of the unique-existence theorem for that offset map.
Claim. Let $N_x,N_y,N_z\ge 1$ and let $V=\mathbb{Z}/N_x\times\mathbb{Z}/N_y\times\mathbb{Z}/N_z$ be the periodic cubic vertex set. For each offset index $a\in\{0,\ldots,7\}$ and each target $t\in V$, if $c$ denotes the unique base cell such that translating $c$ by the bit triple of $a$ yields $t$, then $t$ equals that translate of $c$.
background
The ambient setting is the physical six-tet cubic Dirichlet instance: the module packages exact obligations needed to instantiate the physical Dirichlet model on an encoded periodic Freudenthal torus, without asserting the physical equality for free.
Vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. The map addVertexBits translates a vertex by the three coordinate bits of an index $a\in\mathrm{Fin},8$. The companion uniqueness theorem states there is a unique cell $c$ with $t=\mathrm{addVertexBits}(c,a)$ for any fixed $a$ and target $t$. The definition periodicMatchingBaseCell is exactly that unique cell, obtained by classical choice from the uniqueness theorem.
proof idea
One-line term proof. Apply Classical.choose_spec to existsUnique_addVertexBits_eq a target and take the first component of the resulting pair (the equality witness). Uniqueness is not needed for this direction; it is already baked into the definition of the chosen base cell.
why it matters
This specification is the algebraic hinge that lets fiber and stencil constructions name the unique base cell for a given local offset. Downstream it feeds freudenthalExplicitFiberPairSelectedCell_base_eq (recovering the edge base from the selected cell), freudenthalExplicitFiber_localEdgeOf_eq_edge (matching local edges to periodic edges), and sum_ite_eq_of_addVertexBits_apply (collapsing a guarded sum over cells to the single matching term).
In the gravity stack this is scaffolding for the periodic Freudenthal torus realization of the six-tet cubic Dirichlet model, which sits under the Regge cubic-lattice limit and the physical finite-difference Dirichlet action. It does not itself touch the T0–T8 forcing chain, but it is part of the discrete geometry that carries the eight-tick / cubic structure into continuum gravity limits.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.