Geometry Freudenthal Two Cube Strip Global Sq Edge

The global square-edge assignment

A Freudenthal triangulation cuts a cube into six tetrahedra by drawing all diagonals from one corner. When two unit cubes share a square face, the two triangulations must agree along that face, or the combined object is not a coherent mesh. The declaration globalSqEdge assigns a real number to each of the 33 unique edges in this two-cube strip, and the surrounding theorems prove that this assignment is consistent across every tetrahedron.

The construction starts with 12 vertices and 12 tetrahedra, six per cube. Each tetrahedron has six edges, giving 72 local edge slots, but shared face edges appear twice. The library deduplicates the five edges on the common face, leaving 33 global edges. The key theorem, local_sqEdge_eq_global, states that for any tetrahedron and any of its six edge slots, the local square-edge value equals the global one. A companion theorem, edgeInTet_vertices, confirms that the two vertices of any local edge match the two vertices of the corresponding global edge, possibly swapped.

This is the first concrete multi-cube incidence instance beyond a single cube. It establishes that the framework's edge-slot bookkeeping, the discrete record of which edges belong to which tetrahedra, works when two cells meet. The proof is fully machine-checked: the declarations twoCubeStrip_edgeSlotPartition and twoCubeStrip_edgeSlotBookkeeping package the consistency and partition results into reusable structures.

The declaration does not claim anything about the physical meaning of the square-edge value. It assigns numbers to edges, but it does not say what those numbers represent, whether lengths, energies, or something else. It also does not extend to three or more cubes, nor does it address curved or non-cubic cells. The result is purely combinatorial and geometric: a consistent numbering exists for this specific two-cube configuration.

def globalSqEdge : E → ℝ
  | 0 => 1
  | 1 => 1
  | 2 => 1
  | 3 => 2
  | 4 => 2
  | 5 => 2
  | 6 => 3
  | 7 => 1
  | 8 => 1
  | 9 => 2
  | 10 => 1
  | 11 => 1
  | 12 => 2
  | 13 => 1
  | 14 => 1
  | 15 => 1
  | 16 => 2
  | 17 => 1
  | 18 => 1
  | 19 => 1
  | 20 => 2
  | 21 => 2
  | 22 => 3
  | 23 => 1
  | 24 => 1
  | 25 => 2
  | 26 => 1
  | 27 => 2
  | 28 => 1
  | 29 => 1
  | 30 => 2
  | 31 => 1
  | 32 => 1
  | ⟨n+33, h⟩ => absurd h (by omega)

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 ⊢

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

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

What this page does not claim

The declaration does not assign any physical meaning to the square-edge numbers. The result does not extend beyond two cubes to longer strips or other polyhedra. The theorem does not address curved cells or non-cubic triangulations.

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: