CardinalitySpectrumCert
CardinalitySpectrumCert defines a record whose fields witness that spatial dimension equals 3, configuration dimension equals 5, and that gap45, eightTick, and cubeFaces are generated from these via the standard RS multipliers. Researchers checking numerical consistency across the Recognition Science stack would cite the structure to confirm that the canonical list of 20 cardinalities is strictly ordered and bounded by 3125. The record is assembled from reflexivity on the base constants together with the equality lemmas for the composite counts
claimLet $D_s=3$ and $D_c=5$. Set gap$_{45}=D_s^2 D_c$, eightTick$=2^{D_s}$, cubeFaces$=2 D_s$. The structure asserts $360=$ eightTick$cdot$gap$_{45}$, $70=binom{8}{4}$, $125=D_c^3$, $3125=D_c^5$, that the list of canonical RS cardinalities has length 20, is strictly increasing, and that every entry is at most 3125
background
The CrossDomain.CardinalitySpectrum module collects cardinalities that arise from the small generators 2 and 3 together with configuration dimension 5. Dspatial is defined as the spatial dimension fixed at 3. Dconfig is defined as the configuration dimension fixed at 5. rsSpectrum is the explicit list [2, 3, 4, 5, 6, 7, 8, 10, 12, 15, 16, 25, 45, 64, 70, 125, 216, 256, 360, 3125]. Upstream definitions give eightTick as 8, cubeFaces as 6, and twoFace as 2. The module states that every member of the spectrum admits a decomposition into RS primitives and that the spectrum is structured rather than random.
proof idea
The declaration is a structure type whose fields are the required witnesses. Instantiation of the record uses reflexivity on the base constants Dspatial and Dconfig together with the equality lemmas gap45_eq, eightTick_eq and cubeFaces_eq for the derived quantities. The spectrum length, ordering and bound are witnessed directly by the list definition.
why it matters in Recognition Science
CardinalitySpectrumCert supplies the certificate that RS cardinalities form a closed structured set generated from the spatial and configuration dimensions. It is instantiated by the downstream definition cardinalitySpectrumCert. The construction supports the module claim that RS produces a structured numerical spectrum, linking to the eight-tick octave with period 2^3 and the spatial dimension D=3. It touches the question of whether the spectrum exhausts all canonical numbers arising from the phi-ladder.
scope and limits
- Does not establish that the listed spectrum is complete for all RS constructions
- Does not derive the individual numbers from the J-cost functional equation
- Does not provide physical units or interpretations for the cardinalities
- Does not connect the spectrum to the alpha inverse band or mass formula
formal statement (Lean)
119structure CardinalitySpectrumCert where
120 Dspatial_is_3 : Dspatial = 3
121 Dconfig_is_5 : Dconfig = 5
122 gap_as_D : gap45 = Dspatial^2 * Dconfig
123 eightTick_as_D : eightTick = 2 ^ Dspatial
124 cubeFaces_as_D : cubeFaces = twoFace * Dspatial
125 full_turn : (360 : ℕ) = eightTick * gap45
126 choose_central : (70 : ℕ) = Nat.choose 8 4
127 D_cubed : (125 : ℕ) = Dconfig^3
128 D_fifth : (3125 : ℕ) = Dconfig^5
129 spectrum_length : rsSpectrum.length = 20
130 spectrum_pairwise : rsSpectrum.Pairwise (· < ·)
131 spectrum_bounded : ∀ n ∈ rsSpectrum, n ≤ 3125
132