Geometry Periodic Freudenthal Torus Canonical Edge Slot Eq Some Of No Dup

The edge slot guarantee

A ledger is a discrete record of events, and in a tetrahedral mesh the events are edges meeting tetrahedra. The declaration canonicalEdgeSlot_eq_some_of_noDup proves a bookkeeping guarantee: when a tetrahedron's six local edges are all distinct, asking for the slot of a global edge in that tetrahedron always returns an answer, never a blank. The answer is the unique local face number whose edge equals the global one.

The proof rests on two facts. First, the function that finds an edge's slot is total: if the edge genuinely belongs to the tetrahedron, the lookup succeeds. Second, the lookup is consistent: if it returns a slot, that slot's edge really is the one sought. The declaration combines these into the statement that for any periodic Freudenthal torus with all local edges distinct, the canonical edge slot query is defined for every edge in every tetrahedron.

This matters because the mesh's geometry code needs to know, for each edge, which tetrahedra touch it and through which face. Without the guarantee, a lookup could fail at runtime, leaving a hole in the incidence data. The theorem closes that hole for the canonical periodic tiling, so the rest of the framework can rely on the edge-to-tetrahedron bookkeeping being complete.

The declaration does not claim that every edge appears in every tetrahedron, nor that the mesh is finite. It only covers the canonical periodic Freudenthal torus, not arbitrary triangulations. It also does not prove that the edge slots are unique across different tetrahedra; that is a separate incidence property.

theorem canonicalEdgeSlot_eq_some_implies
    {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
    {e : PeriodicEdge Nx Ny Nz} {cell : Vertex Nx Ny Nz}
    {tet : Fin 6} {f : Fin 6}
    (h : canonicalEdgeSlot? e cell tet = some f) :
    e = localEdgeOf cell tet f := by
  unfold canonicalEdgeSlot? at h
  split_ifs at h with h0 h1 h2 h3 h4 h5
  · cases h
    exact h0
  · cases h
    exact h1
  · cases h
    exact h2
  · cases h
    exact h3
  · cases h
    exact h4
  · cases h
    exact h5

What this page does not claim

The theorem does not prove that every edge belongs to every tetrahedron. It does not establish uniqueness of edge slots across different tetrahedra. It applies only to the canonical periodic Freudenthal torus, not to arbitrary triangulations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Geometry/PeriodicFreudenthalTorus.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: