pith. machine review for the scientific record. sign in
def definition def or abbrev high

totalHingesSimp

show as:
view Lean formalization →

The definition totalHingesSimp computes the total hinge count in the Freudenthal simplicial refinement of the unit cube by adding the twelve original edges to the thirteen new hinges. Researchers certifying zero-deficit angles around those hinges in three-dimensional Recognition Science constructions would cite this quantity. It arises as a direct arithmetic sum of two prior constants.

claimLet $H$ be the total number of hinges in the simplicial refinement of the unit cube. Then $H := 12 + 13$, where $12$ counts the edges of the unit cube and $13$ counts the new hinges consisting of twelve face diagonals together with one body diagonal.

background

The Freudenthal triangulation decomposes the unit cube $[0,1]^3$ into six congruent tetrahedra that share the body diagonal. The original cube supplies twelve edges. The refinement adds thirteen new hinges (twelve face diagonals plus the body diagonal), each asserted to carry zero deficit angle because the surrounding dihedral angles sum to $2π$ (six tetrahedra at the body diagonal, four at each face diagonal). The module records only the combinatorial counts needed for this certificate.

proof idea

The definition is a one-line wrapper that adds the value of cubeEdges to the value of newHinges.

why it matters in Recognition Science

This count is invoked by the downstream theorem totalHinges_eq to obtain the equality 25. It supplies the numerical input required to certify that all new hinges have zero deficit angle, a key combinatorial step in the Freudenthal certificate for the three-dimensional case (D=3) inside the Recognition Science framework. The zero-deficit property guarantees local flatness of the simplicial complex.

scope and limits

formal statement (Lean)

  49def totalHingesSimp : ℕ := cubeEdges + newHinges

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (4)

Lean names referenced from this declaration's body.