axisWitnessEdge
plain-language theorem explainer
Concrete positive-displacement periodic edge on the 5×5×5 witness torus: base vertex (1,0,0) and axis displacement class 0. Gravity and Regge auditors cite it as the fixed geometric edge for endpoint-unit fiber sums and for refuting mixed hinge-deficit identities at axis class 0. The body is a one-line structure literal.
Claim. Let $N_x=N_y=N_z=5$. The axis witness edge is the positive-displacement periodic edge on the $N_x\times N_y\times N_z$ torus with base vertex $(1,0,0)$ and displacement index $0\in\{0,\ldots,6\}$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not grant the physical Dirichlet equality for free; it supplies concrete lattice data and theorem-shaped targets against which those equalities can be checked or refuted.
A periodic edge is a positive-displacement edge on the torus, recorded by its lower (base) vertex and one of the seven positive cube displacements (disp : Fin 7). The witness lattice sizes are fixed abbreviations $N_x=N_y=N_z=5$, large enough for nontrivial fiber bookkeeping yet small enough for native decision and explicit closed-form audits.
Displacement class 0 is the pure axis class used throughout the Freudenthal axis-disp-0 fiber analysis (endpoint-unit potentials, local pair fibers, and mixed hinge-deficit targets).
proof idea
Pure definition: a structure literal for PeriodicEdge on the witness sizes, with base := (1, 0, 0) and disp := 0. No lemmas or tactics.
why it matters
This edge is the geometric anchor for the axis-class-0 witness suite. Downstream it pins endpoint identities (axisWitness_edge_endpoints), base-offset and selected-cell uniqueness for local Freudenthal pairs, and equality of explicit fiber pair summands with the local closed form.
It is the edge fed to the endpoint-unit counterexamples that kill the per-disp explicit-fiber closed-form target and the flat unfolded mixed hinge-deficit target at axis class 0 (fiber sum $-4$ forces LHS $4$ while RHS is $0$). Those false targets are part of the obligation package that connects the periodic Freudenthal scaffold to the physical six-tet cubic Dirichlet model, so the witness must be fully explicit and decidable.
In the broader gravity chain this sits under Regge cubic-lattice and Freudenthal length-chain work: a fixed, auditable edge on which continuum-style Dirichlet or hinge identities can be stress-tested before any continuum limit claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.