Geometry Periodic Freudenthal Torus Canonical Encoded Periodic Tet Verts Add Ver

The encoded torus

A torus is a surface shaped like a doughnut, and a tetrahedral mesh fills a three-dimensional region with tetrahedra, the simplest solid shapes. A periodic Freudenthal torus is a standard way to tile a torus with tetrahedra, repeating a pattern in three directions. The Recognition Science declaration canonicalEncodedPeriodic_tetVerts_addVertexBits is about how to encode such a mesh compactly and unambiguously.

Think of each vertex of the mesh as a point in a three-dimensional grid, with coordinates along the three axes. The declaration establishes that any vertex can be reached from any other by adding a small offset: either zero, one, or two steps along each axis, chosen from eight possibilities. The key theorem, existsUnique_addVertexBits_eq, proves that for any target vertex and any of the eight offset choices, there is exactly one starting vertex that, after applying that offset, lands on the target. In other words, the encoding is a perfect one-to-one matching: no two starting vertices collide, and every target is covered.

The proof rests on two simpler facts. First, adding a true bit (a step of one) to a coordinate is an injective operation: it never maps two different coordinates to the same result. Second, adding a false bit (a step of zero) does nothing. Together these show that the whole offset operation is both injective and surjective, hence bijective. The library also proves a related summation identity, sum_ite_eq_of_addVertexBits, which says that if you sum a constant over all starting vertices, but only count the one that maps to a given target, you get exactly that constant. This is a technical tool used in later arguments about the mesh's geometry.

This encoding is part of a larger framework. The library defines a structure EncodedPeriodicFreudenthalTorus that bundles the mesh data with a proof that the edge slots are partitioned correctly, a condition needed for the nonlinear Regge first-variation theorem. The declaration itself does not build a concrete finite mesh; that remains an open target. It only provides the typed model and the uniqueness guarantee for the vertex encoding, which is a necessary step toward that goal.

theorem existsUnique_addVertexBits_eq
    {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (a : Fin 8) (target : Vertex Nx Ny Nz) :
    ∃! cell : Vertex Nx Ny Nz, target = addVertexBits cell a := by
  rcases addVertexBits_surjective a target with ⟨cell, hcell⟩
  refine ⟨cell, hcell.symm, ?_⟩
  intro other hother
  exact addVertexBits_injective a (hother.symm.trans hcell.symm)

theorem addBit_true_injective {N : ℕ} [NeZero N] :
    Function.Injective (fun i : Fin N => addBit i true) := by
  intro i j h
  ext
  have hval : (i.val + 1) % N = (j.val + 1) % N := by
    simpa [addBit, bit] using congrArg Fin.val h
  have hi : i.val + 1 < N ∨ i.val + 1 = N := by
    omega
  have hj : j.val + 1 < N ∨ j.val + 1 = N := by
    omega
  cases hi with
  | inl hi_lt =>
      have himod : (i.val + 1) % N = i.val + 1 := Nat.mod_eq_of_lt hi_lt
      cases hj with
      | inl hj_lt =>
          have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
          omega
      | inr hj_eq =>
          have hjmod : (j.val + 1) % N = 0 := by
            rw [hj_eq, Nat.mod_self]
          omega
  | inr hi_eq =>
      have himod : (i.val + 1) % N = 0 := by
        rw [hi_eq, Nat.mod_self]
      cases hj with
      | inl hj_lt =>
          have hjmod : (j.val + 1) % N = j.val + 1 := Nat.mod_eq_of_lt hj_lt
          omega
      | inr hj_eq =>
          omega

/-- Summing a constant over the unique periodic cell solving a translated
base-vertex equation returns that constant. -/
theorem sum_ite_eq_of_addVertexBits
    {Nx Ny Nz : ℕ} [NeZero Nx] [NeZero Ny] [NeZero Nz]
    (a : Fin 8) (target : Vertex Nx Ny Nz) (c : ℝ) :
    (∑ cell : Vertex Nx Ny Nz,
      if target = addVertexBits cell a then c else 0) = c := by
  classical
  rcases addVertexBits_surjective a target with ⟨cell0, hcell0⟩
  rw [Finset.sum_eq_single cell0]
  · simp [hcell0]
  · intro cell _ hne
    have hneq : target ≠ addVertexBits cell a := by
      intro h
      apply hne
      exact addVertexBits_injective a (h.symm.trans hcell0.symm)
    simp [hneq]
  · intro hnot
    exact (hnot (Finset.mem_univ cell0)).elim

What this page does not claim

The declaration does not construct a concrete finite mesh of a periodic Freudenthal torus. The declaration does not prove any physical or geometric property of the torus beyond the vertex encoding uniqueness. The declaration does not establish the existence of the edge slot partition; that is a separate structure.

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: