Geometry Freudenthal Two Cube Strip

The two-cube strip

The Freudenthal triangulation is a standard way to divide a cube into six tetrahedra without overlaps or gaps, a routine tool in computational geometry. The two-cube strip takes two unit cubes that share one square face and applies that same division to each. The shared face is triangulated identically from both sides, so the tetrahedra meet along the common square without conflict.

Counting the parts gives the shape of the problem. Twelve vertices, twelve tetrahedra, and thirty-three distinct edges: the shared face is where the counting gets interesting. Each cube alone contributes its own edges, but the five edges on the shared face belong to both cubes. A naive count would double them; the correct global count removes that duplication.

In Recognition Science, this construction is a ledger, a discrete record of which pieces touch which. The framework's machine-checked library of formal theorems proves that every local edge slot in every tetrahedron maps to exactly one global edge, and that this mapping is consistent after the five shared face edges are deduplicated. The theorems local_sqEdge_eq_global and edgeInTet_vertices verify that the local square-edge length and the vertex pairs of each local edge agree with their global representatives.

The result is the first concrete multi-cube incidence instance beyond the one-cube sanity check. It establishes that the local-to-global bookkeeping works when pieces share a face, not just when they sit alone. This matters because the framework's larger geometric claims depend on incidence data being globally consistent.

What the module changes is practical: it turns a bookkeeping worry into a checked fact. Before this, the framework had one cube working in isolation. Now it has two cubes working together, and the shared face is where the real test lay. The next step, already visible in the structure, is to ask what happens when cubes share edges or vertices instead of faces.

def twoCubeStrip : Triangulation3D where
  nV := 12
  nE := 33
  nT := 12
  edgeVerts := edgeVerts
  tetVerts := tetVerts
  edgeInTet := edgeInTet
  tet := fun _ => FreudenthalCubeTriangulation.freudenthalTet

theorem localEdge_complete (τ : T) (f : Fin 6) :
    ∃ e : E, edgeInTet e τ = some f := by
  exact ⟨localEdgeOf τ f, (edgeInTet_iff_localEdgeOf (localEdgeOf τ f) τ f).2 rfl⟩

theorem local_sqEdge_eq_global
    (e : E) (τ : T) (f : Fin 6) (h : edgeInTet e τ = some f) :
    FreudenthalCubeTriangulation.freudenthalTet.sqEdge f = globalSqEdge e := by
  have he : e = localEdgeOf τ f := (edgeInTet_iff_localEdgeOf e τ f).1 h
  subst e
  fin_cases τ <;> fin_cases f <;>
    simp [localEdgeOf, FreudenthalCubeTriangulation.freudenthalTet,
      FreudenthalCubeTriangulation.freudenthalTetSqEdges, globalSqEdge]

theorem edgeInTet_vertices
    (e : E) (τ : T) (f : Fin 6) (h : edgeInTet e τ = some f) :
      let ev := edgeVerts e
      let tv := ReggeRigorousFoundation.edgeVertices f
      (tetVerts τ tv.1 = ev.1 ∧ tetVerts τ tv.2 = ev.2) ∨
        (tetVerts τ tv.1 = ev.2 ∧ tetVerts τ tv.2 = ev.1) := by
  have he : e = localEdgeOf τ f := (edgeInTet_iff_localEdgeOf e τ f).1 h
  subst e
  fin_cases τ <;> fin_cases f <;>
    simp [localEdgeOf, edgeVerts, tetVerts,
      ReggeRigorousFoundation.edgeVertices] at h ⊢

What this page does not claim

This module does not prove that every multi-cube Freudenthal triangulation is globally consistent. This module does not derive any physical constant or dimensional claim. This module does not define what a Freudenthal triangulation is for non-cube polytopes.

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/FreudenthalTwoCubeStrip.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: