pith. machine review for the scientific record. sign in
def definition def or abbrev high

rsSpectrum

show as:
view Lean formalization →

rsSpectrum enumerates the first twenty canonical cardinalities that arise across RS domain types. Cross-domain consistency checks cite this list when confirming that every entry decomposes into the generators 2, 3, 5 and gap45. The definition is a direct literal list of twenty natural numbers.

claimThe RS cardinality spectrum is the ordered list $ [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125] $.

background

The CrossDomain.CardinalitySpectrum module presents the spectrum as a concrete witness that cardinalities of canonical domain types form a structured numerical set rather than an arbitrary collection. Relevant definitions are Dspatial = 3, Dconfig = 5, gap45 = Dspatial² × Dconfig, eightTick = 2^Dspatial and cubeFaces = twoFace × Dspatial; each spectrum member is reachable by multiplication, summation or powering of these primitives together with the small cube-generators {2, 3}. The module setting is Wave 63 Cross-Domain, with the explicit goal of exhibiting decompositions into RS primitives and with zero sorry or axiom.

proof idea

The definition is a direct literal enumeration of the twenty values.

why it matters in Recognition Science

The list supplies the concrete data used by CardinalitySpectrumCert to certify Dspatial = 3, Dconfig = 5, gap45 = Dspatial² × Dconfig, eightTick = 2^Dspatial and cubeFaces = twoFace × Dspatial. It also feeds the boundedness result that every member is ≤ 3125 = D⁵ together with the length and pairwise-ordering theorems. In the Recognition Science framework the definition illustrates the structured spectrum generated by the eight-tick octave and D = 3 spatial dimensions, filling the C21 cross-domain cardinality claim.

scope and limits

formal statement (Lean)

 107def rsSpectrum : List ℕ :=

proof body

Definition body.

 108  [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]
 109

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.