axisWitnessCell
plain-language theorem explainer
Maps each local Freudenthal (tet, edge-slot) pair to a fixed cell on the 5×5×5 witness torus used for the axis-witness edge audit. Gravity and Regge-lattice workers cite it when evaluating flat edge-length directional derivatives and pair summands on that witness. The body is a six-row match table with a default zero cell.
Claim. For each local Freudenthal pair $(t,s)\in\{0,\ldots,5\}^2$, assign a periodic cubic cell in $\mathrm{Fin}\,5\times\mathrm{Fin}\,5\times\mathrm{Fin}\,5$ by the audit table: $(0,0)\mapsto(1,0,0)$, $(1,0)\mapsto(1,0,0)$, $(2,3)\mapsto(1,4,0)$, $(3,5)\mapsto(1,4,4)$, $(4,3)\mapsto(1,0,4)$, $(5,5)\mapsto(1,4,4)$, and all other pairs to $(0,0,0)$.
background
The module packages exact obligations that instantiate the physical six-tet cubic Dirichlet model on an encoded periodic Freudenthal torus. It does not free the physical Dirichlet equality; it isolates finite tables after the periodic-cell base-offset equation is fixed.
A local Freudenthal pair is a pair $(t,s)\in\mathrm{Fin},6\times\mathrm{Fin},6$ (tetrahedron index and edge-slot). Periodic cubic vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. The witness lattice here is the concrete $5\times5\times5$ torus ($N_x=N_y=N_z=5$).
The axis-witness construction needs one matching cell per active local pair so that base offsets, edge vertices, and flat edge-length directional derivatives can be evaluated by pure table lookup rather than by solving placement equations at each use site.
proof idea
Definition by exhaustive pattern match on the two Fin-6 components of the pair. Six active rows return the audit cells $(1,0,0)$, $(1,4,0)$, $(1,4,4)$, $(1,0,4)$ as listed; the catch-all returns the origin cell $(0,0,0)$. No lemmas are invoked.
why it matters
This table is the placement kernel for the axis-witness edge on the physical six-tet cubic Dirichlet instance. Downstream, axisWitnessCell_base_offset proves that for pairs in the displacement-0 fiber the witness edge base equals the cell plus the cube-edge base of the local edge. Flat edge-length directional derivatives (axisWitnessFlatEdgeLengthDir and its equality and vanishing lemmas) and the concrete pair-summand evaluations for $(0,0)$, $(1,0)$, $(2,3)$, etc., all read the cell from this map.
In the broader gravity stack the witness supports the finite-difference Dirichlet action and Hessian-is-Dirichlet certificates that connect the periodic Freudenthal torus scaffold to the physical model target. It is bookkeeping infrastructure, not a forcing-chain step (T0–T8), but without the fixed cells the axis-witness summands cannot be reduced to explicit rationals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.