cubeFaces
plain-language theorem explainer
cubeFaces is defined as the constant 6, equal to twice the spatial dimension Dspatial. Workers on the RS cardinality spectrum cite it to witness the decomposition of spectrum members into the primitives 2 and 3. The assignment is a direct constant definition that matches the geometric face count of the 3-cube Q3. It requires no computation beyond the upstream definition of Dspatial as 3.
Claim. Let $D = 3$ be the spatial dimension. Define the face count of the unit 3-cube by $c := 2D = 6$.
background
Dspatial is defined as the constant 3. The module collects witnesses that spectrum cardinalities admit decompositions into RS primitives {2, 3}, configDim 5, and gap45. Upstream results supply the same constant: ParadigmShiftLattice.cubeFaces states it is the six faces of Q3, while FreudenthalTriangulationCert.cubeFaces states it is the unit cube face count.
proof idea
Direct constant definition assigning 6, with inline comment 2 * Dspatial. No lemmas or tactics are invoked; the value follows immediately from the sibling definition Dspatial := 3.
why it matters
Supplies the value required by CardinalitySpectrumCert (cubeFaces_as_D : cubeFaces = twoFace * Dspatial) and by theorems six_is_cubeFaces and five_plus_one_equals_six. It realizes the T8 forcing step that fixes D = 3 spatial dimensions and contributes the entry 6 to the structured spectrum. It touches the question whether every spectrum member decomposes uniformly into the listed primitives.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.