Geometry Freudenthal Two Cube Strip Two Cube Strip Incidence Consistent

The two-cube strip

Imagine two unit cubes sitting side by side, sharing one square face. A standard way to break a cube into simpler pieces is the Freudenthal triangulation, which slices each cube into six tetrahedra. The two-cube strip is the smallest nontrivial example of this: twelve tetrahedra total, six in each cube, with the triangulations on the shared face forced to match. The construction assigns 12 vertices and 33 distinct edges to the whole strip, then records which tetrahedron uses which edge and in what position.

The declaration twoCubeStrip_incidenceConsistent is a machine-checked proof that this bookkeeping is coherent. It shows that every edge slot in every tetrahedron corresponds to exactly one global edge of the strip, and that the endpoints of a local edge always match the endpoints of its global representative, possibly in reversed order. A companion result proves the stronger claim: the local edge slots partition the global edges without overlap or omission. In plain terms, the strip is a consistent three-dimensional triangulation, not just a pile of tetrahedra with mismatched faces.

This example matters because it is the first multi-cube incidence instance beyond a single cube. The single cube is a sanity check; the two-cube strip tests whether the formalism survives a seam where five edges are shared between the two halves. The proof handles the deduplication of those shared edges, so the global count of 33 edges is correct after merging, not before. The construction is deliberately small, which makes it a clean test case for larger triangulations that would appear in numerical relativity or lattice gauge theory.

In Recognition Science, the framework models physical structure through a discrete ledger of recognition events, and this strip provides a concrete geometric object on which such ledgers can be tested. The framework's machine-checked library of formal theorems uses the strip to verify that its incidence bookkeeping rules hold on a nontrivial shape. The declaration does not prove anything about physics, forces, or the golden ratio; it is a geometric consistency result about a specific triangulation. It also does not claim that the Freudenthal triangulation is the only way to decompose a cube, nor that the strip is the smallest possible multi-cube example in every sense; it is the smallest nontrivial example for this particular construction.

def twoCubeStrip_incidenceConsistent :
    IncidenceConsistent twoCubeStrip where
  globalSqEdge := globalSqEdge
  edgeInTet_vertices := by
    intro e τ f h
    exact edgeInTet_vertices e τ f h
  local_sqEdge_eq_global := by
    intro e τ f h
    exact local_sqEdge_eq_global e τ f h
  localEdge_complete := by
    intro τ f
    exact localEdge_complete τ f
  local_schlaefli := by
    intro τ
    exact schlaefliTetrahedronClosedForm FreudenthalCubeTriangulation.freudenthalTet

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 ⊢

theorem edgeInTet_iff_localEdgeOf (e : E) (τ : T) (f : Fin 6) :
    edgeInTet e τ = some f ↔ e = localEdgeOf τ f := by
  native_decide +revert

def twoCubeStrip_edgeSlotPartition :
    IncidenceEdgeSlotPartition twoCubeStrip twoCubeStrip_incidenceConsistent where
  localEdgeOf := localEdgeOf
  edgeInTet_iff := by
    intro e τ f
    exact edgeInTet_iff_localEdgeOf e τ f

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]

What this page does not claim

The declaration does not prove anything about physics, forces, or the golden ratio. It does not claim the Freudenthal triangulation is the only way to decompose a cube. It does not establish that the strip is the smallest multi-cube example in every possible sense.

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: