def
definition
stepMuTauDerived
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepDerivation on GitHub at line 93.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
90/-! ## The Full Step Formula -/
91
92/-- The Tau Generation Step derived from F, W, D, and α. -/
93noncomputable def stepMuTauDerived : ℝ :=
94 (F : ℝ) - tauStepCoefficientDerived * Constants.alpha
95
96/-- Main Theorem: The derived step matches the definition in Defs.lean. -/
97theorem stepMuTauDerived_matches_def (step_mu_tau_def : ℝ)
98 (h_def : step_mu_tau_def = (F : ℝ) - (2 * (W : ℝ) + 3) / 2 * Constants.alpha) :
99 stepMuTauDerived = step_mu_tau_def := by
100 rw [h_def]
101 unfold stepMuTauDerived
102 rw [tauStepCoefficientDerived_matches_paper]
103
104end TauStepDerivation
105end LeptonGenerations
106end Physics
107end IndisputableMonolith