lemma proved term proof

`alpha_pos_aux`

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

formal statement (Lean)

  53private lemma alpha_pos_aux : 0 < alpha := by

Term-mode proof.

  54  unfold alpha alphaInv alpha_seed; positivity
  55
  56/-- α_W is positive (both α and sin²θ_W are positive). -/

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

alpha_W_gt_alpha in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_gt_two_alpha in IndisputableMonolith.StandardModel.WeakCoupling decl_use
alpha_W_pos in IndisputableMonolith.StandardModel.WeakCoupling decl_use

Lean names referenced from this declaration's body.

alpha in IndisputableMonolith.Constants.Alpha decl_use
alphaInv in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.Alpha decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaHigherOrder decl_use
alpha_seed in IndisputableMonolith.Constants.AlphaPrecision decl_use
is in IndisputableMonolith.Foundation.OptionAEmpiricalProgram decl_use
is in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi decl_use
is in IndisputableMonolith.GameTheory.MechanismDesignFromSigma decl_use
is in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
and in IndisputableMonolith.NumberTheory.CirclePhaseLift decl_use