LargeScaleStructureCert
plain-language theorem explainer
LargeScaleStructureCert records that Recognition Science cosmology admits exactly five large-scale structure regimes whose comoving scales form a geometric sequence with common ratio phi and remain strictly positive. Cosmologists working inside the RS framework cite it to anchor the phi-ladder description that runs from CMB acoustic scales through cosmic voids. The declaration is a plain structure definition that directly enumerates the three required properties.
Claim. A structure asserting that the inductive type of large-scale structure regimes (CMB acoustic, baryon acoustic oscillation, galaxy cluster, filament, cosmic void) has cardinality 5, that the scale function satisfies $s(k+1)/s(k)=phi$ for all natural numbers $k$, and that $s(k)>0$ for every $k$.
background
The module defines five canonical LSS regimes that match configDim D=5: CMB acoustic scale, baryon acoustic oscillation, galaxy clusters, filamentary structure, and cosmic voids. These are collected in the inductive type LSSRegime, which derives Fintype so that its cardinality is automatically 5. The scale function is given by phi raised to the rung index k, placing each regime one step up the phi-ladder in comoving length.
proof idea
The declaration is a structure definition that directly bundles the three certification conditions: the Fintype cardinality of LSSRegime, the constant ratio property expressed with the upstream scale definition, and the strict positivity condition on scale values.
why it matters
The structure is instantiated by largeScaleStructureCert, which supplies the concrete certificate for downstream cosmology arguments. It fills the requirement for five regimes in the RS cosmology depth and aligns with the phi-ladder description of comoving scales. It touches the open question of deriving these regimes from the forcing chain or Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.