axisWitnessCell_base_offset
plain-language theorem explainer
For each local Freudenthal (tet, edge-slot) pair in the zero-displacement fiber, the base vertex of the fixed axis witness edge equals that pair's axis-witness cell shifted by the cube-edge base of its local edge. Lattice-gravity workers instantiating the six-tet cubic Dirichlet model cite this to lock the selected cell. The proof exhausts the six fiber members and closes each case by native decision.
Claim. Let $(t,f)$ be a local Freudenthal tetrahedron/edge-slot pair in the zero-displacement fiber. Then the base vertex of the axis witness edge equals the vertex obtained by adding the cube-edge base bits of the global edge assigned to slot $(t,f)$ onto the axis-witness cell of $(t,f)$.
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; it isolates finite combinatorial identities that the encoded scaffold must satisfy.
A local Freudenthal pair is a pair $(t,f)\in\mathrm{Fin},6\times\mathrm{Fin},6$ naming a tetrahedron and one of its six edge slots. The map localEdgeOf sends each such slot to one of the 19 one-cube Freudenthal edge representatives. Each representative carries a cube-edge base (a local cube vertex in $\mathrm{Fin},8$) and a displacement; on the periodic torus, addVertexBits translates a cell by those base bits to produce the global edge base.
The zero-displacement fiber freudenthalLocalPairDispFiber 0 is the finite set of local pairs whose associated edge has vanishing displacement. The axis witness edge is a fixed periodic edge used as a matching witness; axisWitnessCell assigns to each fiber pair the candidate base cell that should reconstruct that witness.
proof idea
Membership in the zero-displacement fiber is unfolded to an explicit six-way disjunction: the pair equals one of $(0,0)$, $(1,0)$, $(2,3)$, $(3,5)$, $(4,3)$, $(5,5)$. Case-split on that disjunction (six rfl branches). Each concrete pair is then discharged by native_decide, which evaluates both sides of the base-offset equation on the finite tables for axisWitnessCell, localEdgeOf, cubeEdgeBase, and addVertexBits. No algebraic lemma is needed beyond the fiber membership rewrite.
why it matters
The immediate consumer is axisWitness_selectedCell_eq, which rewrites the explicitly selected fiber cell back to axisWitnessCell by invoking periodic base-cell uniqueness on this offset identity. That step is part of wiring the encoded periodic Freudenthal torus into the physical six-tet cubic Dirichlet target: once the witness edge's base is known to be the cell-plus-cube-base composite, the matching cell is unique and the Dirichlet stencil can be attached without an extra choice.
In the broader gravity stack this sits under the Regge/cubic-lattice limit path (periodic Freudenthal scaffold, finite-difference Dirichlet action, canonical Hessian). It is pure combinatorial bookkeeping on the eight-vertex cube and six-tet decomposition, not a continuum curvature statement, but it is a required closed obligation in the instance package the module advertises.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.