Geometry Periodic Freudenthal Torus

The periodic torus

A torus is the surface of a donut: a shape that loops around on itself in two independent directions. A Freudenthal tiling is a standard way to divide a space into tetrahedra, the three-dimensional building blocks with four triangular faces. A periodic Freudenthal torus combines these ideas: it is a torus built from a repeating pattern of tetrahedra, where the pattern wraps around the two loops of the donut. This structure provides a formal, machine-checked model of this shape and proves a key property about how its edges fit together.

The model starts with a grid of points, labeled by three whole numbers, and defines a torus by making the grid wrap around: moving one step past the end of a row brings you back to the beginning. Each tetrahedron in the tiling is then identified by a grid point and one of six possible orientations. The structure defines the vertices, edges, and tetrahedra of this periodic structure in a precise, typed way, and it proves several basic facts about them, such as that every edge has two distinct endpoints and that the eight corners of a cell are distinct when the grid is large enough.

The central result is that this periodic tiling has a property called an incidence edge slot partition, a way of assigning each edge of each tetrahedron to a unique slot so that no edge is counted twice. The structure proves this for the canonical periodic triangulation, and it also defines a structure for any finite encoding of the torus that guarantees the same property. This matters because the partition is a precondition for a later theorem about how the shape responds to changes in its geometry, a step toward a full theory of how space itself can bend and move.

In Recognition Science, this structure is a piece of the larger project of deriving the structure of space from a ledger of recognition events. The framework treats physical space as a discrete, periodic structure, and this torus is one candidate shape for that structure at a large scale. The structure does not yet provide a concrete finite mesh for the torus, meaning it does not give the exact list of points and connections for a specific size. That remains as future work, but the model and the key property are established.

/-- Periodic cubic vertices. -/
abbrev Vertex (Nx Ny Nz : ℕ) := Fin Nx × Fin Ny × Fin Nz

/-- A positive-displacement periodic edge, represented by its lower/base
vertex and one of the seven positive cube displacements. -/
structure PeriodicEdge (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] where
  base : Vertex Nx Ny Nz
  disp : Fin 7

/-- Periodic Freudenthal tetrahedra: one of the six Freudenthal tetrahedra
inside each periodic cubic cell. -/
abbrev PeriodicTet (Nx Ny Nz : ℕ) := Vertex Nx Ny Nz × Fin 6

def canonicalPeriodicIncidenceConsistent
    (Nx Ny Nz : ℕ) [NeZero Nx] [NeZero Ny] [NeZero Nz] :
    IncidenceConsistent (canonicalPeriodicTriangulation Nx Ny Nz) :=
  canonicalPeriodicIncidenceConsistent_of_endpoint Nx Ny Nz
    (canonicalPeriodicEndpointIncidence Nx Ny Nz)

What this page does not claim

This structure does not provide a concrete finite mesh for the torus. This structure does not prove that physical space is a torus. The incidence property is a precondition, not a statement about the dynamics of the shape.

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: