Geometry Periodic Freudenthal Torus Local Edge Of Endpoints Match Tet Verts

Local edge endpoints

A periodic tetrahedral mesh is a way to fill three-dimensional space with tetrahedra that repeat in every direction, like a crystal lattice. The Recognition Science framework builds such meshes from a small set of typed objects: vertices, edges, and tetrahedra, each carrying a position and a label. The declaration localEdgeOf_endpoints_match_tetVerts is a proved theorem in the framework's machine-checked library of formal theorems. It states that when you take any tetrahedron in the periodic Freudenthal tiling and look at one of its six edges, the two endpoints recorded for that edge are exactly the two vertices of the tetrahedron that the edge connects.

This is a consistency guarantee. In a finite mesh, the same edge can be shared by several tetrahedra, and a careless encoding might record an edge with the wrong pair of vertices, breaking the global structure needed for later computations. The theorem rules out that failure for the canonical periodic Freudenthal torus, the scalable target shape defined in the framework. It proves that the local edge construction, which builds an edge from a cell and a face index, always agrees with the tetrahedron's own vertex list. The proof relies on the underlying definitions: a vertex is a triple of coordinates modulo the period lengths, and an edge is a base vertex plus one of seven displacement directions. The theorem closes the loop between these local pieces and the global incidence structure.

The theorem is one step in a larger argument. The framework's goal is to prove that any finite triangulation encoding this periodic torus has the global IncidenceEdgeSlotPartition needed by the nonlinear Regge first-variation theorem, a tool for discrete gravity. This particular declaration supplies the endpoint match that makes the incidence partition well-defined. It does not, however, provide a concrete finite mesh. The framework explicitly leaves open the construction of a finite encoder from the typed periodic torus into finite index sets. It also does not claim that the periodic Freudenthal tiling is the only possible mesh, or that the Regge theorem itself is proved here. Those remain separate targets.

theorem localEdgeOf_endpoints_match_tetVerts
    {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (cell : Vertex Nx Ny Nz) (tet f : Fin 6) :
      let edge := localEdgeOf cell tet f
      let ev := edge.endpoints
      let tv := ReggeRigorousFoundation.edgeVertices f
      (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.1 ∧
        addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.2) ∨
        (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.2 ∧
          addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.1) := by
  fin_cases tet <;> fin_cases f <;>
    simp [localEdgeOf, PeriodicEdge.endpoints,
      FreudenthalCubeTriangulation.localEdgeOf,
      FreudenthalCubeTriangulation.tetVerts,
      ReggeRigorousFoundation.edgeVertices,
      cubeEdgeBase, cubeEdgeDisp, dispBits, vertexBits, addVertexBits, addBits]

theorem localEdgeOf_endpoints_match_tetVerts
    {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (cell : Vertex Nx Ny Nz) (tet f : Fin 6) :
      let edge := localEdgeOf cell tet f
      let ev := edge.endpoints
      let tv := ReggeRigorousFoundation.edgeVertices f
      (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.1 ∧
        addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.2) ∨
        (addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.1) = ev.2 ∧
          addVertexBits cell (FreudenthalCubeTriangulation.tetVerts tet tv.2) = ev.1) := by
  fin_cases tet <;> fin_cases f <;>
    simp [localEdgeOf, PeriodicEdge.endpoints,
      FreudenthalCubeTriangulation.localEdgeOf,
      FreudenthalCubeTriangulation.tetVerts,
      ReggeRigorousFoundation.edgeVertices,
      cubeEdgeBase, cubeEdgeDisp, dispBits, vertexBits, addVertexBits, addBits]

theorem canonicalPeriodicEndpointIncidence
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
    CanonicalPeriodicEndpointIncidence Nx Ny Nz := by
  intro e τ f h
  have he := canonicalEdgeInTet_eq_some_implies Nx Ny Nz e τ h
  let cell := (tetFinEquiv Nx Ny Nz τ).1
  let tet := (tetFinEquiv Nx Ny Nz τ).2
  have hlocal := localEdgeOf_endpoints_match_tetVerts (Nx := Nx) (Ny := Ny) (Nz := Nz)
    cell tet f
  dsimp [CanonicalPeriodicEndpointIncidence, canonicalEdgeVerts, canonicalTetVerts]
  rw [he]
  rcases hlocal with hdir | hrev
  · left
    constructor
    · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hdir.1
    · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hdir.2
  · right
    constructor
    · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hrev.1
    · exact congrArg (vertexFinEquiv Nx Ny Nz).symm hrev.2

What this page does not claim

The theorem does not construct a concrete finite mesh. The theorem does not prove the nonlinear Regge first-variation theorem itself. The theorem does not assert that the periodic Freudenthal tiling is the only possible periodic mesh.

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: