theorem proved term proof

`alpha_positive`

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

formal statement (Lean)

  34theorem alpha_positive : alpha > 0 := by

Term-mode proof.

  35  unfold alpha alphaInv alpha_seed
  36  positivity
  37
  38/-- **CALCULATED**: α < 0.1 (approximately 1/137 < 0.1). -/

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

inflation_cert in IndisputableMonolith.Gravity.Inflation decl_use
InflationCert in IndisputableMonolith.Gravity.Inflation decl_use
alpha_bounds in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use
constants_predictions_cert_exists in IndisputableMonolith.Unification.ConstantsPredictionsProved decl_use

Lean names referenced from this declaration's body.