twoFace
plain-language theorem explainer
Definition twoFace assigns the natural number 2 as the binary face count inside the RS cardinality spectrum. Researchers verifying decompositions of cube-related numbers into RS generators cite this value when confirming cubeFaces equals twoFace times Dspatial. The entry is a direct constant assignment requiring no further reduction.
Claim. The binary face count is the natural number $2$.
background
The CrossDomain.CardinalitySpectrum module assembles witnesses that cardinalities across the Recognition Science stack form the structured spectrum {2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 45, 70, 125, 216, 256, 3125, ...}. Each entry decomposes via multiplication, summation, or powers of the cube-generators {2, 3}, the configuration dimension 5, and gap45. The module documentation states that every spectrum member admits such a decomposition into RS primitives, with zero sorry or axiom present.
proof idea
Direct definition that binds the constant 2 to twoFace.
why it matters
This definition supplies the binary factor required by the CardinalitySpectrumCert structure, which records Dspatial = 3, Dconfig = 5, gap45 = Dspatial squared times Dconfig, eightTick = 2 to the power Dspatial, and cubeFaces = twoFace times Dspatial. It supports the module's C21 claim that the spectrum arises from RS primitives rather than arbitrarily.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.