localEdge_complete
plain-language theorem explainer
Every local edge slot of every tetrahedron in the Freudenthal six-tet cube is hit by some global edge under the incidence map. Anyone assembling IncidenceConsistent for this triangulation cites it. The proof is a one-line witness: the chosen section localEdgeOf, discharged by the edgeInTet/localEdgeOf equivalence.
Claim. For every tetrahedron index $\tau\in\{0,\ldots,5\}$ and every local edge slot $f\in\{0,\ldots,5\}$, there exists a global edge index $e\in\{0,\ldots,18\}$ such that the incidence map sends $(e,\tau)$ to the local slot $f$.
background
The module builds the standard Freudenthal decomposition of the unit cube into six tetrahedra along the body diagonal from vertex $0=(0,0,0)$ to $7=(1,1,1)$. Cube vertices are binary coordinates; the six tets are the monotone paths from $0$ to $7$.
Global edges are indexed by $\mathrm{Fin},19$. Each tetrahedron has six local edge slots. The map edgeInTet records, for a global edge and a tet, which local slot (if any) that edge occupies. The section localEdgeOf chooses, for each tet and local slot, a concrete global edge that fills it.
The companion lemma edgeInTet_iff_localEdgeOf states that edgeInTet e τ = some f if and only if $e$ equals localEdgeOf τ f. That equivalence is proved by exhaustive fin_cases on the three finite indices.
proof idea
One-line term proof. Witness the existential with localEdgeOf τ f. The second component of the pair is the reverse direction of edgeInTet_iff_localEdgeOf applied at that witness, with rfl discharging the equality hypothesis. No further casework is needed at this site.
why it matters
This is the surjectivity half of the local-to-global edge bookkeeping required by the structure IncidenceConsistent on a Triangulation3D. It is installed directly into freudenthalCube_incidenceConsistent, and the same pattern is copied for the two-cube strip and the periodic Freudenthal torus.
Downstream, ConformalSchlaefliIncidenceBookkeeping in the Regge first-variation module needs a consistent incidence class so that the edge-indexed deficit variation can be rewritten as a sum of local tetrahedral Schläfli identities. Without local-edge completeness, some local dihedral contributions would be missing from the global sum.
In the broader RS geometry stack this sits under discrete 3D scaffolding (T8 forces $D=3$), feeding the path from cube triangulation to global Schläfli without caller-supplied data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.