LSSRegime
plain-language theorem explainer
Recognition Science cosmology enumerates large-scale structure into five regimes aligned with successive rungs on the phi-ladder in comoving length. Researchers certifying the framework's predictions for CMB acoustics through cosmic voids reference this finite classification. The declaration is a direct inductive enumeration deriving Fintype to enable an immediate cardinality decision.
Claim. The large-scale structure regimes consist of the five cases CMB acoustic scale, baryon acoustic oscillation, galaxy cluster, filament, and cosmic void, each separated by a factor of $phi$ along the comoving phi-ladder.
background
The module defines five canonical LSS regimes under configDim D = 5, with each regime occupying one rung up the phi-ladder in comoving length. This classification draws from the Recognition Science forcing chain where phi is the self-similar fixed point and the eight-tick octave governs scaling. The inductive type supplies the finite set whose cardinality is later asserted to equal 5.
proof idea
The declaration is the inductive definition with five constructors and automatic derivation of DecidableEq, Repr, BEq, and Fintype. No separate proof body exists; the Fintype instance is generated directly from the enumeration.
why it matters
This supplies the finite set of regimes required by the LargeScaleStructureCert structure, which asserts Fintype.card LSSRegime = 5 together with the phi_ratio and positivity properties. It fills the enumeration step in the cosmology depth of the Recognition Science framework, connecting directly to the phi-ladder and T7 eight-tick octave. The downstream lssRegime_count theorem confirms the count by decision procedure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.