`bottom_required_phi_exponent`

definition

show as: view math explainer →

module: IndisputableMonolith.Masses.HeavyQuarkFullClosureObstruction
domain: Masses
line: 54 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Masses.HeavyQuarkFullClosureObstruction on GitHub at line 54.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

used by

formal source

  51/-! ## Required extra φ-exponents, evaluated -/
  52
  53def charm_required_phi_exponent : ℝ := 100.60116086852311
  54def bottom_required_phi_exponent : ℝ := 102.02875053742147
  55def top_required_phi_exponent : ℝ := 104.80972375767824
  56
  57theorem required_exponents_not_equal :
  58    charm_required_phi_exponent ≠ bottom_required_phi_exponent ∧
  59    bottom_required_phi_exponent ≠ top_required_phi_exponent ∧
  60    charm_required_phi_exponent ≠ top_required_phi_exponent := by
  61  unfold charm_required_phi_exponent bottom_required_phi_exponent top_required_phi_exponent
  62  norm_num
  63
  64/-- Audit conclusion: there is no single universal extra φ-exponent among the
  65three evaluated heavy-quark channels under the current bridge. -/
  66structure HeavyQuarkClosureObstructionCert where
  67  charm_below : charm_raw_eV < charm_PDG_eV / 1e18
  68  bottom_below : bottom_raw_eV < bottom_PDG_eV / 1e18
  69  top_below : top_raw_eV < top_PDG_eV / 1e18
  70  exponents_split :
  71    charm_required_phi_exponent ≠ bottom_required_phi_exponent ∧
  72    bottom_required_phi_exponent ≠ top_required_phi_exponent ∧
  73    charm_required_phi_exponent ≠ top_required_phi_exponent
  74
  75theorem heavyQuarkClosureObstructionCert_holds :
  76    HeavyQuarkClosureObstructionCert :=
  77{ charm_below := charm_raw_far_below_PDG
  78  bottom_below := bottom_raw_far_below_PDG
  79  top_below := top_raw_far_below_PDG
  80  exponents_split := required_exponents_not_equal }
  81
  82end IndisputableMonolith.Masses.HeavyQuarkFullClosureObstruction

papers checked against this theorem

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