rsSpectrum_length
The theorem asserts that the explicit list of canonical Recognition Science cardinalities contains precisely twenty entries. Cross-domain researchers cite it to anchor the enumeration of values generated from the cube generators, configuration dimension 5, and gap45. The proof reduces immediately to a decision procedure on the list definition.
claimLet $S$ be the list of the first twenty canonical Recognition Science cardinalities. Then $|S| = 20$.
background
The module assembles witnesses showing that RS cardinalities form a structured spectrum rather than an arbitrary collection. The spectrum list is constructed explicitly from operations on the small cube-generators {2, 3}, the configuration dimension 5, and gap45, yielding the sequence [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]. Upstream results supply the list definition together with supporting 'is' statements from OptionAEmpiricalProgram, SimplicialLedger, MechanismDesignFromSigma, and MockThetaPhantom that certify the underlying combinatorial building blocks.
proof idea
The proof is a one-line wrapper that applies the decide tactic directly to the explicit list definition of rsSpectrum.
why it matters in Recognition Science
This length result feeds the cardinalitySpectrumCert definition, which packages the spectrum properties including Dspatial_is_3, Dconfig_is_5, gap_as_D, eightTick_as_D, and cubeFaces_as_D. It completes the C21 structural claim that every listed cardinality admits a decomposition into RS primitives. Within the Recognition framework the result reinforces the eight-tick octave and phi-ladder structures visible in entries such as 8, 16, and 256.
scope and limits
- Does not prove the listed spectrum is exhaustive beyond the twenty enumerated values.
- Does not derive individual cardinalities from the forcing chain or RCL within this statement.
- Does not supply physical interpretations or mass formulas for the entries.
formal statement (Lean)
110theorem rsSpectrum_length : rsSpectrum.length = 20 := by decide
proof body
Term-mode proof.
111
112/-- The spectrum is strictly increasing (pairwise). -/