pith. machine review for the scientific record. sign in
structure definition def or abbrev

InflatonCert

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  64structure InflatonCert where
  65  five_regimes : Fintype.card InflatonRegime = 5
  66  efolds : efoldCount = 44
  67  phi5_fibonacci : phi ^ 5 = 5 * phi + 3
  68  epsilon_pos : 0 < slowRollEpsilon
  69  eta_pos : 0 < slowRollEta
  70  spectral_index_in_band : ((0.955 : ℝ) < 1 - 2/45) ∧ (1 - 2/45 < (0.957 : ℝ))
  71

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.