CardinalitySpectrumCert
plain-language theorem explainer
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
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.