`pi0_error_simplified`

proved

show as: view math explainer →

module: IndisputableMonolith.QFT.Anomalies
domain: QFT
line: 83 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.Anomalies on GitHub at line 83.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

lifetime IndisputableMonolith.Physics.DecaySpectrumFromPhiLadder

formal source

  80  native_decide
  81
  82/-- Simplify: 12/852 = 1/71 -/
  83theorem pi0_error_simplified :
  84    (12 : ℚ) / 852 = 1 / 71 := by
  85  norm_num
  86
  87/-- **THEOREM**: The π⁰ lifetime prediction matches experiment to < 2%. -/
  88theorem pi0_prediction_within_2_percent :
  89    pi0_relative_error_rational < 2/100 := by
  90  rw [pi0_error_computation]
  91  norm_num
  92
  93/-- **THEOREM**: More precisely, the error is about 1.41% (1/71 ≈ 0.0141). -/
  94theorem pi0_error_bound :
  95    (1 : ℚ) / 71 < 15 / 1000 := by
  96  norm_num
  97
  98/-! ## QCD Asymptotic Freedom -/
  99
 100/-- QCD one-loop beta function coefficient. -/
 101def qcdBetaCoeff (Nc Nf : ℕ) : ℚ := (11 * Nc - 2 * Nf) / 3
 102
 103/-- **THEOREM**: QCD (Nc=3) with 6 flavors has positive beta coefficient. -/
 104theorem qcd_beta_nf6 :
 105    qcdBetaCoeff 3 6 = 7 := by
 106  native_decide
 107
 108/-- **THEOREM**: Positive beta means asymptotically free. -/
 109theorem qcd_asymptotic_freedom_nf6 :
 110    qcdBetaCoeff 3 6 > 0 := by
 111  rw [qcd_beta_nf6]
 112  norm_num
 113

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.