rsSpectrum_pairwise_lt
plain-language theorem explainer
The list of canonical Recognition Science cardinalities is strictly increasing. Cross-domain cardinality analyses would cite this to confirm the ordered spectrum values. The proof is a one-line decision procedure that checks all pairwise inequalities on the explicit finite list.
Claim. Let $S = [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]$ be the list of canonical Recognition Science cardinalities. Then $S$ is pairwise strictly increasing: for all indices $i < j$, the $i$-th entry is less than the $j$-th entry.
background
The module collects exemplar witnesses for the RS cardinality spectrum, a structured list of values reachable by multiplying, summing, or powering the cube-generators {2, 3}, the configuration dimension 5, and gap45. The definition rsSpectrum enumerates the first 20 such cardinalities explicitly, each tied to RS primitives rather than chosen arbitrarily.
proof idea
The proof is a one-line decision procedure that verifies the pairwise strict inequalities directly on the finite list of natural numbers.
why it matters
This result supports the cardinalitySpectrumCert definition, which certifies spectrum properties including spatial dimension 3 and configuration dimension 5. It fills the structural claim that spectrum members admit decompositions into RS primitives, consistent with the eight-tick octave and phi-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.