vertCoord
plain-language theorem explainer
Extracts the three real coordinates of a vertex on the periodic cubic torus as its representative in [0,N)³. Downstream TT Bloch and midpoint-phase constructions cite it whenever a plane-wave phase needs a geometric base point. The body is a three-branch pattern match on Fin 3 that casts each Fin N component to ℝ.
Claim. For a periodic cubic vertex $x \in \{0,\ldots,N-1\}^3$, the map $\mathrm{vertCoord}(x):\{0,1,2\}\to\mathbb{R}$ returns the three real coordinates of the representative of $x$ in the half-open cube $[0,N)^3$.
background
The ambient lattice is the periodic Freudenthal torus: vertices are triples of residue classes Vertex N N N := Fin N × Fin N × Fin N. Geometry and Regge calculus on this torus need ordinary real base points, not modular indices, so each vertex is read as its unique representative in the fundamental domain $[0,N)^3$.
This module builds the true nonlinear 3D Regge action and the TT Bloch symbol object for the QG full-theory campaign (Stage 1). Plane-wave edge fields and midpoint phases are written as $k\cdot(x+D_d/2)$; the $x$ factor is exactly these real coordinates.
Upstream, Vertex is the standard periodic cubic vertex type. Displacement and edge data live on the same torus; coordinate extraction is the bridge from discrete indices to the real inner products that define Bloch phases.
proof idea
Definition by cases on the coordinate index $i\in\mathrm{Fin},3$. Component $0$ is the first Fin N cast to $\mathbb{R}$; component $1$ is the middle factor; component $2$ is the last. No lemmas are invoked; it is pure structural projection plus coercion.
why it matters
Without real vertex coordinates, the preregistered midpoint Bloch phase $k\cdot(x+D_d/2)$ cannot be stated on the periodic geometry. The sibling edgeMidpointPhase is built directly from this map, and the grounding theorem edgeMidpointPhase_grounded (Gate B bridge) checks that the doubled-midpoint table matches the actual geometry at $N=4$.
Bloch assembly also uses it: vertCoord_addVertexBits records how coordinates transform when a cube-vertex bit offset is added, including the modular wrap by $N$. That identity feeds plane-wave and TT-symbol constructions aimed at the open continuum target ReggeTTContinuumIsotropyTarget (isotropic $K(0)=-(1/4)I_{TT}$ matching linearized Einstein-Hilbert TT).
In the broader RS gravity stack this is scaffolding for the Regge TT continuum symbol program, not a forcing-chain step (T0–T8), but it is the coordinate interface those continuum claims sit on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.