theorem proved term proof

`r_at_55_bounds`

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

formal statement (Lean)

  55theorem r_at_55_bounds : tensor_to_scalar 55 > 0 := by

proof body

Term-mode proof.

  56  unfold tensor_to_scalar
  57  apply div_pos
  58  · exact mul_pos (by norm_num) alpha_attractor_pos
  59  · positivity
  60
  61/-- For N = 55: n_s ≈ 0.964. -/

depends on (3)

Lean names referenced from this declaration's body.

tensor_to_scalar in IndisputableMonolith.Cosmology.PrimordialSpectrum decl_use
alpha_attractor_pos in IndisputableMonolith.Gravity.Inflation decl_use
tensor_to_scalar in IndisputableMonolith.Gravity.Inflation decl_use