Geometry Freudenthal Cube Triangulation Freudenthal Cube Incidence Consistent

The incidence record

The standard Freudenthal decomposition divides a unit cube into six tetrahedra using the body diagonal from vertex 0 to vertex 7. Each tetrahedron is a monotone path from one end of that diagonal to the other, and each has three unit step edges, two face diagonals, and one body diagonal. This is a classical construction in computational geometry, used in finite element meshing and piecewise linear interpolation.

The declaration freudenthalCube_incidenceConsistent is a machine-checked proof that this triangulation's incidence bookkeeping is coherent. Incidence here means the record of which edges belong to which tetrahedra, and in which local slot. The proof establishes three properties: every global edge that appears in a tetrahedron maps to a unique local slot; every local slot in every tetrahedron is filled by exactly one global edge; and the squared length of a global edge equals the squared length of its corresponding local edge. The first property is proved by edgeInTet_iff_localEdgeOf, the second by localEdge_complete, and the third by local_sqEdge_eq_global.

In Recognition Science, this declaration is a concrete instance of a more general framework concept: the ledger, a discrete record of events with forced consistency. Here the events are edge-tetrahedron incidences, and the framework's library proves that the Freudenthal cube's record has no duplication and no gaps. The nondegeneracy of each tetrahedron is separately established by the theorem cm3_freudenthalTetSqEdges, which shows the Cayley-Menger determinant is 8, a positive value.

What this declaration does not claim is broader geometric or physical significance. It does not prove that the Freudenthal triangulation is the only way to decompose a cube, nor that it has any special property beyond incidence consistency. It does not claim that the cube's triangulation relates to the framework's forcing chain, its constants, or its particle ladder. The declaration is a local, self-contained bookkeeping result: a finite combinatorial object checked to be internally consistent.

/-- Incidence consistency for the Freudenthal cube. -/
def freudenthalCube_incidenceConsistent :
    IncidenceConsistent freudenthalCube 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 freudenthalTet

theorem edgeInTet_iff_localEdgeOf
    (e : Fin 19) (τ f : Fin 6) :
    edgeInTet e τ = some f ↔ e = localEdgeOf τ f := by
  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
    simp [edgeInTet, localEdgeOf]

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

theorem local_sqEdge_eq_global
    (e : Fin 19) (τ f : Fin 6) (h : edgeInTet e τ = some f) :
    freudenthalTet.sqEdge f = globalSqEdge e := by
  fin_cases e <;> fin_cases τ <;> fin_cases f <;>
    simp [edgeInTet, freudenthalTet, freudenthalTetSqEdges, globalSqEdge] at h ⊢

theorem cm3_freudenthalTetSqEdges :
    CayleyMengerPolynomial.cm3 freudenthalTetSqEdges = 8 := by
  unfold freudenthalTetSqEdges CayleyMengerPolynomial.cm3
  norm_num

What this page does not claim

The declaration does not prove the Freudenthal triangulation is unique or optimal among cube decompositions. It does not connect the cube triangulation to the framework's forcing chain, constants, or particle ladder. It does not establish any property of the triangulation beyond incidence consistency and nondegeneracy.

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