WitnessNy

The module packages exact theorem 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 concrete finite-grid data and matching lemmas.

Vertices and periodic edges on that torus are typed by three natural periods $(N_x, N_y, N_z)$. Downstream axis-witness constructions (cells, edges, endpoints, unit potentials) all take these three sizes as parameters. The present abbreviation pins the middle size.

Sibling names in the same file include the canonical Hessian-is-Dirichlet certificate, periodic edge-stencil Dirichlet actions, and mixed-axis stencil targets; all of those live on the same finite torus whose y-period is this constant.

Definitional abbreviation: WitnessNy is definitionally equal to the natural number literal 5. No lemmas, tactics, or obligations.

Supplies the concrete y-period used by the entire axis-witness family in this module: axisWitnessCell, axisWitnessEdge, axisWitnessEndpoint0/1, axisWitnessEndpointUnitPotential, and the apply lemmas that evaluate that potential. Those objects are the audit table and test potentials that connect the encoded periodic Freudenthal torus scaffold to the PhysicalSixTetCubicDirichletModel target.

In the broader gravity chain this sits under the Regge cubic-lattice limit and Freudenthal length-chain endpoint certificates imported by the module. The choice $N_y = 5$ is part of a fixed finite witness large enough to host the six-tet cubic stencil and the axis-aligned local pairs without self-loops; it is scaffolding data, not a derived physical constant from the T0–T8 forcing chain.