axisWitness_selectedCell_eq
plain-language theorem explainer
For every local Freudenthal (tet, edge-slot) pair in the displacement-0 fiber, the unique periodic cell selected by the explicit fiber construction on the axis witness edge equals the hand-tabulated axis witness cell. Gravity auditors use this to justify the audit table against the general matching-cell operator. The proof unfolds the selected-cell definition and invokes uniqueness of the periodic matching base cell from the already-proved base-offset identity.
Claim. Let a local Freudenthal pair be a pair $(t,s)\in\{0,\ldots,5\}^2$. If $(t,s)$ lies in the explicit displacement-class-$0$ fiber, then the unique periodic matching base cell of the axis witness edge (base $(1,0,0)$, displacement $0$) at that pair equals the tabulated axis-witness cell of $(t,s)$.
background
This module packages the exact obligations needed to instantiate the physical six-tet cubic Dirichlet model on a periodic Freudenthal torus; it does not assert the physical Dirichlet equality for free.
A local Freudenthal pair is a finite $(tet, edge\text{-}slot)$ index in $\mathrm{Fin},6\times\mathrm{Fin},6$, the residual table after the periodic-cell base-offset equation is isolated. The displacement fiber for class $0$ is an explicit six-element finset of such pairs. The axis witness edge is the typed periodic edge with base $(1,0,0)$ and displacement $0$. The axis witness cell is a hand-written matching-cell table on that fiber (e.g. $(0,0)\mapsto(1,0,0)$, $(2,3)\mapsto(1,4,0)$).
The general selected-cell operator returns the unique periodic matching base cell of a typed edge at a local pair. Upstream, axisWitnessCell_base_offset already shows that the tabulated cell satisfies the base-offset equation for the axis witness edge on the class-$0$ fiber.
proof idea
Term-mode, three steps. Unfold the definition of the explicit fiber selected-cell operator, which is just the unique periodic matching base cell of the local cube edge. Symmetrize the goal so the tabulated cell is on the left. Discharge by periodicMatchingBaseCell_unique applied to the already-proved base-offset identity axisWitnessCell_base_offset pair hp, which witnesses that the tabulated cell solves the same matching equation.
why it matters
Feeds the private lemma that equates the closed-form expanded fiber summand on the axis witness edge to the local axis-witness pair summand. That step is part of wiring the encoded periodic Freudenthal torus scaffold into the physical six-tet cubic Dirichlet target: the audit table for the axis edge must agree with the general selected-cell operator before summands can be rewritten.
In the broader gravity chain this sits under the Regge cubic lattice / Freudenthal length-chain endpoint certificates imported by the module. It is bookkeeping uniqueness, not a new continuum limit, but without it the axis-witness audit path cannot be identified with the canonical fiber construction used for the Dirichlet stencil.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.