cubeFaces_eq
plain-language theorem explainer
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.
Claim. The 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.