rsSpectrum
plain-language theorem explainer
rsSpectrum supplies the explicit list of the first twenty canonical cardinalities that appear across RS domain types. Cross-domain consistency checks in Recognition Science cite this list when confirming that cardinalities remain bounded by D^5 and strictly ordered. The definition is a direct enumeration with no lemmas or computation.
Claim. The RS cardinality spectrum is the ordered list $S = [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]$.
background
Module C21 states that cardinalities of canonical domain types across the RS stack form a structured spectrum rather than arbitrary values. Each entry is reachable by multiplication, summation, or powers of the cube-generators {2, 3}, the configuration dimension 5, and gap45. Sibling definitions fix Dspatial = 3, Dconfig = 5, gap45 = Dspatial² · Dconfig, eightTick = 2^Dspatial, and cubeFaces = twoFace · Dspatial.
proof idea
Definition by explicit list literal. No lemmas or tactics are invoked; the body is the concrete sequence of twenty naturals.
why it matters
The list is the concrete object used by CardinalitySpectrumCert (which records Dspatial_is_3, Dconfig_is_5, gap_as_D, eightTick_as_D, cubeFaces_as_D) and by the three immediate theorems rsSpectrum_bounded, rsSpectrum_length, rsSpectrum_pairwise_lt. It realizes the C21 claim that the spectrum is generated from RS primitives and connects to the eight-tick octave (T7) and D = 3 (T8). It leaves open whether the listed members exhaust all RS cardinalities.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.