rsSpectrum_bounded
plain-language theorem explainer
The theorem asserts that every cardinality in the Recognition Science spectrum is at most 3125. Cross-domain cardinality analysts cite it to confirm the spectrum stays finite and controlled by the configuration dimension. A single decision procedure on the explicit finite list discharges the claim.
Claim. Every member $n$ of the Recognition Science spectrum satisfies $n ≤ 3125$, where 3125 equals the fifth power of the configuration dimension.
background
The module collects canonical cardinalities generated by RS primitives: spatial dimension 3, configuration dimension 5, and gap45. The definition rsSpectrum enumerates the first twenty such values, including 5^5 = 3125 at the end of the list. This theorem sits directly above that definition and supplies the explicit upper bound used by the downstream certification structure.
proof idea
The proof is a one-line wrapper that applies the decide tactic to the finite list of spectrum members, verifying the inequality for each entry by direct computation.
why it matters
This bound supports the cardinalitySpectrumCert definition that assembles the spectrum witnesses. It fills the cross-domain claim that RS produces a structured numerical spectrum whose members remain within D^5. The result confirms that constructions built from the small cube-generators and gap45 stay inside a computable range.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.