Foundation Freudenthal Triangulation Cert Total Hinges Eq

The hinge count

The Freudenthal triangulation is a classical way to cut the unit cube [0,1]³ into six congruent tetrahedra. The cube has 8 vertices, 12 edges, and 6 faces. The decomposition adds 13 new internal segments: the 12 face diagonals and the 1 body diagonal that all six tetrahedra share. The declaration totalHinges_eq in the framework's machine-checked library of formal theorems records a simple arithmetic consequence: the total number of hinges, meaning the original edges plus the new diagonals, is 25. That is the entire content of the declaration, a counting fact proved by direct computation.

The certificate also records why the new hinges matter geometrically. Around the body diagonal, six tetrahedra meet, each at a dihedral angle of π/3, and six times π/3 is 2π, a full turn with zero deficit angle. Around each face diagonal, four tetrahedra tile the full 2π, again with zero deficit. The certificate packages these as a structure named ZeroDeficitCert, whose fields assert that both deficits are zero and that the new hinge count is 13. The whole certificate, FreudenthalCert, bundles the cube counts, the tetrahedron count, the hinge count, the angle sum, and the zero-deficit assertions into one machine-checked object with no unproved axioms.

What the declaration does not claim is just as precise. It does not assert that the Freudenthal triangulation is the only way to decompose a cube, nor that zero deficit angles make a decomposition physically realizable as a rigid linkage. The certificate proves the arithmetic and the angle-sum identities; it does not prove that a physical hinge mechanism can be built from these segments. The zero-deficit fields are stated as True, which in the formal library means the statement is accepted as an axiom-free placeholder, not derived from a geometric model of physical hinges. The declaration totalHinges_eq itself is only the equation 12 + 13 = 25, nothing more.

In the Recognition Science framework, this certificate is a combinatorial check within a larger forcing chain. The framework models recognition events as discrete records, and the cube decomposition appears as a structural example of how a three-dimensional cell can be refined without introducing angular defects at the new internal edges. The certificate does not by itself force three dimensions; that forcing is a separate theorem elsewhere in the library. What this declaration establishes is a clean, verified counting statement that any later argument can rely on without rechecking the arithmetic.

theorem totalHinges_eq : totalHingesSimp = 25 := by decide

/-- Sum of 6 × (1/6) = 1 (symbolic angle check). -/
theorem body_diagonal_full_angle : 6 * (1 : ℚ) / 6 = 1 := by norm_num

def freudenthalCert : FreudenthalCert where
  cube_data := ⟨rfl, rfl, rfl⟩
  tet_count := freudenthal_count
  new_hinges := rfl
  body_angle := body_diagonal_full_angle
  zero_deficit := zeroDeficitCert

What this page does not claim

The certificate does not prove that a physical hinge mechanism can be built from these segments. The zero-deficit fields are stated as True, not derived from a geometric model of physical hinges. This declaration does not by itself force three dimensions.

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/Foundation/FreudenthalTriangulationCert.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: