`predicted_mass`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.QuarkMasses
domain: Physics
line: 91 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Physics.QuarkMasses on GitHub at line 91.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  88-/
  89
  90/-- Predicted Mass Formula: m = m_struct * phi^res. -/
  91noncomputable def predicted_mass (res : ℚ) : ℝ :=
  92  electron_structural_mass * (phi ^ (res : ℝ))
  93
  94def H_top_mass_match : Prop :=
  95  abs (predicted_mass res_top - mass_top_exp) / mass_top_exp < 0.0005
  96
  97def H_bottom_mass_match : Prop :=
  98  abs (predicted_mass res_bottom - mass_bottom_exp) / mass_bottom_exp < 0.01
  99
 100def H_charm_mass_match : Prop :=
 101  abs (predicted_mass res_charm - mass_charm_exp) / mass_charm_exp < 0.02
 102
 103/-- **CERTIFICATE (HYPOTHESIS LANE)**: Quark Quarter-Ladder matches (top/bottom/charm). -/
 104structure QuarkMassCert where
 105  top_match : H_top_mass_match
 106  bottom_match : H_bottom_mass_match
 107  charm_match : H_charm_mass_match
 108
 109theorem quark_mass_verified
 110    (h_top : H_top_mass_match)
 111    (h_bottom : H_bottom_mass_match)
 112    (h_charm : H_charm_mass_match) : QuarkMassCert :=
 113  { top_match := h_top, bottom_match := h_bottom, charm_match := h_charm }
 114
 115end QuarkMasses
 116end Physics
 117end IndisputableMonolith

papers checked against this theorem

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