`pi0_error_bound`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.QFT.Anomalies on GitHub at line 94.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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
 114/-- **THEOREM**: With 17 flavors, beta coefficient is negative. -/
 115theorem qcd_beta_nf17 :
 116    qcdBetaCoeff 3 17 = -1/3 := by
 117  native_decide
 118
 119/-- **THEOREM**: Negative beta means NOT asymptotically free. -/
 120theorem qcd_no_af_nf17 :
 121    qcdBetaCoeff 3 17 < 0 := by
 122  rw [qcd_beta_nf17]
 123  norm_num
 124

papers checked against this theorem

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