`charm_threshold`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.RunningCouplings
domain: Physics
line: 288 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.RunningCouplings on GitHub at line 288.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 285  h_pos : 0 < scale
 286  h_step : n_f_below + 1 = n_f_above
 287
 288def charm_threshold : FlavorThreshold where
 289  scale := 1.27
 290  n_f_below := 3
 291  n_f_above := 4
 292  h_pos := by norm_num
 293  h_step := by norm_num
 294
 295def bottom_threshold : FlavorThreshold where
 296  scale := 4.18
 297  n_f_below := 4
 298  n_f_above := 5
 299  h_pos := by norm_num
 300  h_step := by norm_num
 301
 302def top_threshold : FlavorThreshold where
 303  scale := 172.69
 304  n_f_below := 5
 305  n_f_above := 6
 306  h_pos := by norm_num
 307  h_step := by norm_num
 308
 309/-- Multi-segment mass transport: run a mass from μ₁ to μ₂ through
 310    a list of flavor thresholds, switching n_f at each crossing. -/
 311noncomputable def transport_mass_through
 312    (m_ref : ℝ) (α_s_at : ℝ → ℝ) (μ_start μ_end : ℝ)
 313    (thresholds : List FlavorThreshold) (n_f_init : ℕ) : ℝ :=
 314  match thresholds with
 315  | [] => running_mass m_ref (α_s_at μ_start) (α_s_at μ_end) n_f_init
 316  | thr :: rest =>
 317    if μ_end ≤ thr.scale then
 318      running_mass m_ref (α_s_at μ_start) (α_s_at μ_end) n_f_init

papers checked against this theorem

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