axisWitness_edge_endpoints
plain-language theorem explainer
On the concrete N=5 periodic Freudenthal witness, the axis-class edge with base (1,0,0) and displacement 0 has endpoints exactly the designated endpoint pair. Counterexample theorems that refute closed-form and flat-unfolded explicit-fiber identities at axis class 0 cite this equality to pin the edge they evaluate. The proof is a one-line native_decide on the fixed witness data.
Claim. For the witness periodic edge with base $(1,0,0)$ and displacement class $0$ on the $N=5$ torus, the ordered pair of endpoints equals the designated endpoint pair $\bigl((1,0,0),\,v_1\bigr)$, where $v_1$ is the second axis-witness endpoint vertex.
background
This 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 supplies the concrete witness data and the identities needed to connect the scaffold to the model target.
The axis witness edge is the periodic edge with base $(1,0,0)$ and displacement class $0$. Its two endpoint vertices are named separately as the ordered pair used throughout the endpoint-unit counterexample (base $(1,0,0)$, $N=5$), matching the audit script for per-pair axis-class-$0$ contributions. Endpoints of a periodic edge are the ordered pair of lattice vertices joined by that edge on the torus.
Downstream refutations evaluate mixed-hinge and explicit-fiber targets on this same edge and potential, so the endpoint equality must be available as a proved fact rather than an informal convention.
proof idea
Term-mode proof by native_decide. Both sides are closed concrete terms on the fixed finite witness torus ($N=5$ dimensions and the hard-coded base and displacement), so the kernel decides equality of the endpoint pair by computation. No algebraic lemmas are invoked.
why it matters
The equality is the bookkeeping link that lets later theorems name the axis-class-$0$ edge and its endpoints interchangeably. It is used by the refutations that the per-disp explicit-fiber closed-form mixed identity fails at axis class $0$ (fiber sum $-4$ forces LHS $4$ while RHS is $0$), that the flat-unfolded explicit-fiber target fails on the same witness, and that the bilinear endpoint template at disp $0$ is incompatible with the global endpoint-unit fiber-sum witness.
In the gravity stack this sits inside the periodic Freudenthal / Regge cubic-lattice path toward the physical six-tet Dirichlet model: concrete counterexamples on the witness torus close off incorrect closed-form fiber templates before any claim of physical Dirichlet equality. It is local geometry bookkeeping, not a forcing-chain (T0–T8) step, but it keeps the Dirichlet-instance obligations honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.