Geometry Freudenthal Two Cube Strip Two Cube Strip Edge Slot Bookkeeping

Edge slot bookkeeping

A Freudenthal triangulation cuts a cube into six tetrahedra along its diagonals. When two unit cubes share a square face, the combined shape, called a two-cube strip, holds twelve tetrahedra: six in each cube. The shared face contributes edges that appear in both cubes, so the strip has 12 vertices, 12 tetrahedra, but only 33 distinct global edges after those five shared face edges are counted once.

The declaration twoCubeStrip_edgeSlotBookkeeping establishes that this local-to-global edge accounting is consistent. Each of the 72 local edge slots, six per tetrahedron, maps to exactly one of the 33 global edges, and no global edge is left out. The bookkeeping is a ledger, a discrete record of which local edge belongs to which global edge, and the declaration proves the record is complete and unambiguous.

This is the first concrete multi-cube incidence example beyond the single-cube sanity check. It verifies that the framework's machinery for tracking edges, which underpins how geometry is represented in the Recognition Science library, works when shapes share faces, not just in isolation.

The declaration does not claim anything about the physical shape or size of the cubes, nor about the tetrahedra's internal angles. It is purely combinatorial: it concerns which edges touch which tetrahedra, not how those edges sit in space. It also does not derive any physical constants or laws; it is a definitional consistency check within a geometric model.

def twoCubeStrip_edgeSlotBookkeeping :
    IncidenceEdgeSlotBookkeeping twoCubeStrip twoCubeStrip_incidenceConsistent :=
  incidenceEdgeSlotBookkeeping_of_partition
    twoCubeStrip twoCubeStrip_incidenceConsistent twoCubeStrip_edgeSlotPartition

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

def twoCubeStrip_edgeSlotBookkeeping :
    IncidenceEdgeSlotBookkeeping twoCubeStrip twoCubeStrip_incidenceConsistent :=
  incidenceEdgeSlotBookkeeping_of_partition
    twoCubeStrip twoCubeStrip_incidenceConsistent twoCubeStrip_edgeSlotPartition

What this page does not claim

No claim about the physical geometry, angles, or lengths of the edges is made. No physical constants or laws are derived from this bookkeeping. The declaration does not address how the edge slots relate to the framework's cost function or forcing chain.

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: