cubeFaces
The definition assigns the constant 6 to cubeFaces as twice the spatial dimension. Researchers verifying the Recognition Science cardinality spectrum would cite it when confirming decompositions of spectrum members into primitives 2 and 3. It is a direct constant definition that supports equality theorems and the spectrum certificate without further computation.
claimLet cubeFaces denote the number of faces of the three-dimensional cube $Q_3$. Then cubeFaces equals 6.
background
The CrossDomain.CardinalitySpectrum module collects witnesses for the structured spectrum of cardinalities in Recognition Science, including members reachable from generators {2, 3}, configuration dimension 5, and gap45. Dspatial is defined as 3, matching the spatial dimension forced by the eight-tick octave. Upstream results supply parallel definitions: cubeFaces as six faces of $Q_3$ in ParadigmShiftLattice and as unit cube face count in FreudenthalTriangulationCert.
proof idea
This is a direct definition that sets cubeFaces to the constant 6. It functions as a one-line abbreviation relying on the prior definition of Dspatial as 3.
why it matters in Recognition Science
The definition feeds the CardinalitySpectrumCert structure via the field cubeFaces_as_D : cubeFaces = twoFace * Dspatial. It supports downstream theorems including six_is_cubeFaces, cubeFaces_eq, and twoSixteen_is_six_cubed, plus five_plus_one_equals_six in ParadigmShiftLattice. It instantiates the spatial dimension D = 3 from T8 and anchors the spectrum decomposition into RS primitives.
scope and limits
- Does not derive the value 6 from the forcing chain axioms.
- Does not claim uniqueness of this face count across all RS domains.
- Does not address higher-dimensional cube analogs.
- Does not connect the definition to constants such as alpha or G.
Lean usage
theorem six_is_cubeFaces : (6 : ℕ) = cubeFaces := rflformal statement (Lean)
31def cubeFaces : ℕ := 6 -- 2 * Dspatial
proof body
Definition body.
32