IndisputableMonolith.Physics.CosmologicalPerturbationFromRS

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4/-!
   5# Cosmological Perturbation Theory from RS — S3 Cosmology Depth
   6
   7Cosmological perturbations seed structure formation.
   8Five canonical perturbation types (scalar, vector, tensor, isocurvature, entropy)
   9= configDim D = 5.
  10
  11RS: the primordial power spectrum P(k) ∝ k^(n_s-1) with n_s ∈ (0.95, 0.96).
  12(proved in InflationEfoldsFromGap45.lean)
  13
  14The 5 perturbation types are excited by the 5 recognition degrees of freedom
  15at the RS inflation threshold.
  16
  17Lean: 5 types.
  18
  19Lean status: 0 sorry, 0 axiom.
  20-/
  21
  22namespace IndisputableMonolith.Physics.CosmologicalPerturbationFromRS
  23open Constants
  24
  25inductive PerturbationType where
  26  | scalar | vector | tensor | isocurvature | entropy
  27  deriving DecidableEq, Repr, BEq, Fintype
  28
  29theorem perturbationTypeCount : Fintype.card PerturbationType = 5 := by decide
  30
  31structure CosmoPerturbCert where
  32  five_types : Fintype.card PerturbationType = 5
  33
  34def cosmoPerturbCert : CosmoPerturbCert where
  35  five_types := perturbationTypeCount
  36
  37end IndisputableMonolith.Physics.CosmologicalPerturbationFromRS
  38