theorem proved term proof

`alpha_seed_positive`

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

formal statement (Lean)

  60theorem alpha_seed_positive : 0 < alpha_seed := by

Term-mode proof.

  61  unfold alpha_seed
  62  have hpi : 0 < Real.pi := Real.pi_pos
  63  linarith
  64
  65/-- The exponential formula produces a positive value. -/

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

alphaInv_positive in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
exp_factor_bounded in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
log_alphaInv_eq in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
logarithmic_derivative_constant in IndisputableMonolith.Constants.AlphaExponentialForm decl_use
alpha_precision_cert_exists in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_positive in IndisputableMonolith.Constants.AlphaPrecision decl_use

Lean names referenced from this declaration's body.

alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
alpha_seed_positive in IndisputableMonolith.Constants.AlphaPrecision decl_use
value in IndisputableMonolith.QFT.SpinStatistics decl_use