lssRegime_count
plain-language theorem explainer
Recognition Science cosmology enumerates exactly five large-scale structure regimes from CMB acoustics through cosmic voids. Modelers working inside the phi-ladder framework cite this cardinality when certifying the complete set of canonical scales. The proof is a one-line decision procedure that exploits the automatically derived Fintype instance on the five-constructor inductive type.
Claim. The set of large-scale structure regimes has cardinality five: $|$CMB acoustic scale, baryon acoustic oscillation, galaxy cluster, filament, cosmic void$| = 5$.
background
The module introduces five canonical regimes for large-scale structure, each placed one rung higher on the phi-ladder in comoving length and tied to configuration dimension D = 5. LSSRegime is the inductive enumeration whose constructors are cmbAcoustic, baryonAcousticOscillation, galaxyCluster, filament and cosmicVoid; the type automatically carries DecidableEq, Repr, BEq and Fintype instances. The upstream inductive definition supplies the finite set whose cardinality is computed here.
proof idea
One-line wrapper that invokes decide on the Fintype.card computation for the inductive type with five constructors.
why it matters
This supplies the five_regimes field inside largeScaleStructureCert, which assembles the full certification of regimes together with the phi ratio and positivity. It realizes the framework claim that configDim D equals five and closes the enumeration step required by the LargeScaleStructureFromRS development.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.