WitnessNz
plain-language theorem explainer
Fixes the z-period of the witness lattice at five cells for the physical six-tet cubic Dirichlet instance on a periodic Freudenthal torus. Gravity and discrete-geometry proofs that build axis-witness edges, cells, and unit potentials cite this constant so the torus dimensions stay uniform. It is a one-line natural-number abbreviation with no proof obligations.
Claim. The witness lattice period in the $z$-direction is the natural number $N_z = 5$.
background
The module packages exact theorem obligations that 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 only supplies the finite lattice data and matching certificates needed by that target.
Vertices on the torus are triples in a product of finite cycles whose lengths are the three witness periods. The $z$-period appears in every Vertex, PeriodicEdge, and potential typed over those periods, so a single named constant keeps the axis-witness constructions coherent.
Sibling abbreviations fix the companion $x$- and $y$-periods and the corresponding edge lengths; together they determine the discrete domain on which the canonical Hessian and finite-difference Dirichlet action are evaluated.
proof idea
One-line abbreviation equating the witness $z$-period to the natural number five. No lemmas or tactics are involved.
why it matters
Every axis-witness object in the module is indexed by this period: the witness edge, its two endpoints, the matching cells per local Freudenthal pair, and the unit potential supported on those endpoints all take WitnessNz as a type parameter. Downstream lemmas such as the evaluation identity for that unit potential therefore inherit a concrete five-cell $z$-cycle.
In the broader Recognition gravity stack this supplies the finite cubic lattice on which the six-tet Regge action is compared with the continuum Dirichlet energy, feeding the physical model target rather than a free-floating scaffold. It does not itself close the Dirichlet equality; it only freezes the lattice size used by those certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.