canonicalPeriodicTypedEdgeLocalEdgeOfWitness_decidable
plain-language theorem explainer
Decidability of the canonical typed-incidence witness relating a periodic edge to a periodic tetrahedron on the Freudenthal torus. Gravity and Regge-lattice code that must case-split or compute edge-in-tet incidence cites this instance. The proof unfolds the witness definition and synthesizes Decidable from its Boolean building blocks.
Claim. For $N_x,N_y,N_z\ge 1$ and any periodic edge $e$ and periodic tetrahedron $\tau$ on the $N_x\times N_y\times N_z$ Freudenthal torus, the proposition that $e$ is the geometric local edge of $\tau$ under the canonical typed incidence witness is decidable.
background
The module packages exact obligations needed to 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 only assembles the finite combinatorial data and theorem hooks that model requires.
A PeriodicEdge is a positive-displacement edge on the torus, given by a base vertex and one of seven cube displacements. A PeriodicTet is a translated Freudenthal tetrahedron. The geometric map localEdgeOf sends a cell, tet index, and local edge slot to the corresponding global periodic edge (via the cube triangulation table).
The witness canonicalPeriodicTypedEdgeLocalEdgeOfWitness is the Prop asserting that a given edge matches that geometric local-edge image for a given cell-tet. Downstream Dirichlet stencil and Hessian constructions need this Prop to be decidable so incidence can be computed rather than assumed.
proof idea
One-line style instance proof: unfold the witness definition, then infer_instance. After unfolding, the goal is Decidable of a proposition built from equality and structure projections on finite types (PeriodicEdge, PeriodicTet, Fin indices), all of which already carry Decidable instances, so typeclass search closes automatically.
why it matters
Inside the gravity stack this is plumbing, not a physical law: without decidable typed incidence, the periodic edge-stencil Dirichlet action and related Hessian/Dirichlet targets cannot be evaluated or certified by computation on the torus scaffold.
The module's role is to connect the encoded periodic Freudenthal torus to PhysicalSixTetCubicDirichletModel. This instance is a prerequisite for any constructive use of the canonical typed-edge witness in that packaging. No downstream theorems currently list it as a direct parent (used_by is empty), so it sits as infrastructure under the six-tet cubic Dirichlet instantiation rather than a cited scientific lemma.
It does not touch T0–T8, the RCL, or continuum limits; those enter only after the discrete Dirichlet model is fully instantiated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.