WitnessNx
plain-language theorem explainer
Fixes the x-period of the witness cubic lattice at five cells. Gravity and discrete-geometry proofs that build the axis witness edge, endpoints, and unit potential on the encoded periodic Freudenthal torus cite this constant. The body is a one-line natural-number abbreviation.
Claim. The witness lattice period in the $x$-direction is the natural number $N_x = 5$.
background
The module packages exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not assert the physical Dirichlet equality for free; it supplies the finite lattice data and matching lemmas that the model target demands.
Vertices on that torus are triples in a product of cyclic groups of orders $N_x$, $N_y$, $N_z$. The axis witness construction (edge, endpoints, unit potential, matching cells) is written against those periods. This abbreviation pins the $x$-period to five so every downstream vertex, edge, and potential is well-typed on a concrete finite grid.
proof idea
Pure definitional abbreviation: the identifier is definitionally equal to the natural number five. No lemmas, tactics, or proof obligations.
why it matters
Every axis-witness object in the module is parameterized by this period: the witness edge at base $(1,0,0)$, endpoints $(1,0,0)$ and $(2,0,0)$, the unit potential supported on those endpoints, the matching-cell table for local Freudenthal pairs, and the apply lemmas that evaluate the potential. Those objects feed the larger program of connecting the encoded periodic Freudenthal torus scaffold to the physical six-tet cubic Dirichlet model (finite-difference Dirichlet action and Hessian targets on the cubic lattice). Without a fixed finite $N_x$, the vertex type and periodic-edge stencil are not closed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.