rsSpectrum
plain-language theorem explainer
rsSpectrum enumerates the first twenty canonical cardinalities that arise across RS domain types. Cross-domain consistency checks cite this list when confirming that every entry decomposes into the generators 2, 3, 5 and gap45. The definition is a direct literal list of twenty natural numbers.
Claim. The RS cardinality spectrum is the ordered list $ [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125] $.
background
The CrossDomain.CardinalitySpectrum module presents the spectrum as a concrete witness that cardinalities of canonical domain types form a structured numerical set rather than an arbitrary collection. Relevant definitions are Dspatial = 3, Dconfig = 5, gap45 = Dspatial² × Dconfig, eightTick = 2^Dspatial and cubeFaces = twoFace × Dspatial; each spectrum member is reachable by multiplication, summation or powering of these primitives together with the small cube-generators {2, 3}. The module setting is Wave 63 Cross-Domain, with the explicit goal of exhibiting decompositions into RS primitives and with zero sorry or axiom.
proof idea
The definition is a direct literal enumeration of the twenty values.
why it matters
The list supplies the concrete data used by CardinalitySpectrumCert to certify Dspatial = 3, Dconfig = 5, gap45 = Dspatial² × Dconfig, eightTick = 2^Dspatial and cubeFaces = twoFace × Dspatial. It also feeds the boundedness result that every member is ≤ 3125 = D⁵ together with the length and pairwise-ordering theorems. In the Recognition Science framework the definition illustrates the structured spectrum generated by the eight-tick octave and D = 3 spatial dimensions, filling the C21 cross-domain cardinality claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.