Geometry Freudenthal Two Cube Strip Two Cube Strip Edge Slot Partition

The two-cube strip

Take two unit cubes that share one square face. Slice each cube into six tetrahedra using the standard Freudenthal triangulation, which divides a cube by its diagonals. The result is a strip of twelve tetrahedra with a shared face in the middle. This object matters in computational geometry because it is the simplest case where two separate pieces of a mesh meet, and their edge structures must agree along the boundary.

The classical question is whether the local edges of each tetrahedron can be matched to global edges of the whole strip. Each tetrahedron has six edges, so the twelve tetrahedra have 72 local edge slots. The strip has only 33 distinct global edges because edges on the shared face and on the outer boundary are counted once, not twice. The declaration twoCubeStrip_edgeSlotPartition establishes a bijection between every local edge slot and a global edge, after deduplicating the five edges that lie on the shared face. This is a bookkeeping fact: it says the local view and the global view of the mesh agree exactly.

The proof is machine-checked in the framework's library of formal theorems. The key lemma states that a global edge appears in a tetrahedron exactly when it is assigned to that slot, and the assignment respects the vertices of the edge. A second lemma confirms that every one of the 72 local slots has a global edge assigned to it, so nothing is left dangling. The partition is then packaged as a structure that satisfies the incidence consistency conditions, and from it the library derives the full edge-slot bookkeeping record.

In Recognition Science, this is the first concrete multi-cube incidence instance beyond the single-cube sanity check. The framework models physical structure through a discrete record of recognition events, and this declaration provides the smallest nontrivial example where two cubes force a consistent edge accounting across their shared face. It does not claim anything about three spatial dimensions, about the golden ratio, or about any physical law. It is a combinatorial and geometric fact about a specific triangulation, verified by exhaustive case analysis.

The consequence is practical: any algorithm that needs to walk the edges of a two-cube mesh, or to transfer data between local tetrahedral views and a global mesh, can rely on this partition as a verified foundation. The same pattern scales to larger multi-cube strips, and this two-cube case is the proof that the bookkeeping mechanism works when pieces meet.

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

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

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⟩

What this page does not claim

The declaration does not assert anything about physical space or dimensionality. It does not involve the golden ratio, the cost function, or any constants from the forcing chain. It does not claim the partition is unique among all possible triangulations of the two-cube strip.

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: