rsSpectrum_length
plain-language theorem explainer
The theorem confirms that the explicit list of the first twenty canonical cardinalities arising in Recognition Science has length exactly twenty. Cross-domain analysts cite this to anchor the spectrum's initial segment before invoking the certification structure. The verification proceeds by a single decision tactic applied to the concrete list definition.
Claim. Let $S$ be the list enumerating the first twenty canonical cardinalities in the Recognition Science spectrum. Then the length of $S$ equals 20.
background
Module C21 assembles witnesses showing that cardinalities of canonical RS domain types form a structured spectrum generated from the cube-generators {2, 3}, configDim 5, and gap45. The definition rsSpectrum supplies the concrete initial segment [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]. This construction sits inside the cross-domain setting where each entry admits a decomposition into RS primitives, including Fibonacci numbers via the phi-ladder.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the equality on the explicit list rsSpectrum.
why it matters
This length statement supports the downstream cardinalitySpectrumCert, which records the concrete equalities Dspatial = 3, Dconfig = 5, gap45, eightTick, and cubeFaces. It realizes the C21 claim that the spectrum is not arbitrary but built from RS primitives, consistent with the eight-tick octave and D = 3 from the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.