CardinalitySpectrumCert
plain-language theorem explainer
CardinalitySpectrumCert bundles equalities fixing Dspatial to 3, Dconfig to 5, and the derived gap45, eightTick, and cubeFaces, together with the numerical checks that 360 equals their product, 70 is the central binomial, 125 and 3125 are the third and fifth powers of 5, and that rsSpectrum is a strictly increasing list of length 20 bounded by 3125. Cross-domain consistency checks in Recognition Science cite the structure to confirm the listed cardinalities arise from the core dimensions without extraneous generators. The structure is populated
Claim. A structure $C$ such that $D_ {spatial}=3$, $D_{config}=5$, $gap_{45}=D_{spatial}^2 D_{config}$, $eightTick=2^{D_{spatial}}$, $cubeFaces=twoFace D_{spatial}$, $360=eightTick gap_{45}$, $70=binom{8}{4}$, $125=D_{config}^3$, $3125=D_{config}^5$, the list $rsSpectrum$ has length 20, is strictly increasing, and every entry is at most 3125.
background
The module defines Dspatial as the spatial dimension equal to 3 and Dconfig as the configuration dimension equal to 5. These generate twoFace equal to 2, eightTick equal to 8, cubeFaces equal to 6, and gap45 via the equality lemmas. The rsSpectrum list collects the twenty values 2,3,4,5,6,7,8,10,12,15,16,25,45,64,70,125,216,256,360,3125 that decompose into products and powers of these primitives. The module documentation states the point is to show that RS produces a structured numerical spectrum, not a random one, with every member admitting a decomposition into RS primitives. This structure assembles the relations that follow from the eight-tick octave and D equals 3 in the forcing chain.
proof idea
Structure definition whose fields are satisfied by reflexivity on the constants Dspatial and Dconfig together with the sibling equality lemmas gap45_eq, eightTick_eq, cubeFaces_eq and direct computation for the binomial, powers, list length, pairwise ordering, and boundedness checks.
why it matters
The structure supplies the certificate type instantiated by cardinalitySpectrumCert, which witnesses the structured spectrum across the RS stack. The module documentation emphasizes that the cardinalities fall into a specific spectrum reachable by operations on the cube-generators and configDim 5. This supports the forcing chain landmarks T7 eight-tick octave and T8 D equals 3 by confirming the numerical consequences of Dspatial equals 3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.