theorem proved term proof

`spectral_index_lt_one`

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

formal statement (Lean)

  41theorem spectral_index_lt_one : 1 - 2 / (phi ^ 3) < 1 := by

proof body

Term-mode proof.

  42  have h1 : phi ^ 3 > 0 := pow_pos Constants.phi_pos 3
  43  have h2 : 2 / (phi ^ 3) > 0 := div_pos (by norm_num) h1
  44  linarith
  45
  46/-- **CALCULATED**: n_s > 0.5 since φ³ > 4 implies 2/φ³ < 0.5. -/

used by (2)

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

cosmological_predictions_cert_exists in IndisputableMonolith.Unification.CosmologicalPredictionsProved decl_use
spectral_index_bounds in IndisputableMonolith.Unification.CosmologicalPredictionsProved decl_use

depends on (1)

Lean names referenced from this declaration's body.

Constants in IndisputableMonolith.CPM.LawOfExistence decl_use