cubeFaces_eq
The unit cube carries exactly six faces in the Freudenthal triangulation certificate. Recognition Science researchers assembling the cardinality spectrum cite this equality to fix the combinatorial input for D = 3. The proof is a direct reflexivity step that matches the local definition of cubeFaces to the numeral 6.
claimThe number of faces of the unit cube $Q_3$ equals 6.
background
The Freudenthal Triangulation Certificate module records the standard combinatorial counts for the unit cube $[0,1]^3$: eight vertices, twelve edges, and six faces. The sibling definition cubeFaces : ℕ := 6 supplies the face count directly. Upstream results in CardinalitySpectrum and ParadigmShiftLattice introduce the same value as 2 * D_spatial, where D_spatial = 3, aligning with the eight-tick octave and the T8 forcing step that sets spatial dimension to three.
proof idea
The proof is a one-line wrapper that applies reflexivity to the definition of cubeFaces.
why it matters in Recognition Science
This equality populates the cubeFaces_as_D field inside the CardinalitySpectrumCert definition, which collects the full spectrum including Dspatial_is_3. It supplies the combinatorial anchor for the Recognition Science forcing chain at T8 where D = 3. The module doc-comment notes that the Lean formalisation contains zero sorry or axiom statements.
scope and limits
- Does not prove the geometric decomposition into tetrahedra.
- Does not compute dihedral angles or deficit angles at hinges.
- Does not address the phi-ladder or Recognition Composition Law.
- Does not extend the count to higher-dimensional hypercubes.
Lean usage
cubeFaces_as_D := cubeFaces_eqformal statement (Lean)
32theorem cubeFaces_eq : cubeFaces = 6 := rfl
proof body
Term-mode proof.
33
34/-- Freudenthal decomposition: 6 tetrahedra. -/