`top_threshold`

definition

show as: view math explainer →

module: IndisputableMonolith.Physics.RunningCouplings
domain: Physics
line: 302 · 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 302.

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

 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
 319    else
 320      let m_at_thr := running_mass m_ref (α_s_at μ_start) (α_s_at thr.scale) n_f_init
 321      transport_mass_through m_at_thr α_s_at thr.scale μ_end rest thr.n_f_above
 322
 323end RG
 324end Physics
 325end IndisputableMonolith

papers checked against this theorem

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