 134    `HiggsEFTBridge.NormalizationHypothesis`.  It states that the Yukawa
 135    coupling extracted from `m_f` and `v` via `y_f = √2 m_f / v` is the
 136    same as the Yukawa appearing in the SM Lagrangian. -/
 137def YukawaNormalizationHypothesis
 138    (sector : Anchor.Sector) (rung Z : ℤ) (v y_SM : ℝ) : Prop :=
 139  yukawa_SM sector rung Z v = y_SM
 140
 141/-- Under the normalisation hypothesis, the SM-extracted Yukawa is positive. -/
 142theorem yukawa_SM_pos_of_hypothesis
 143    (sector : Anchor.Sector) (rung Z : ℤ) (v y_SM : ℝ) (hv : 0 < v)
 144    (hY : YukawaNormalizationHypothesis sector rung Z v y_SM) :
 145    0 < y_SM := by
 146  unfold YukawaNormalizationHypothesis at hY
 147  have h := yukawa_SM_pos sector rung Z v hv
 148  rw [← hY]; exact h
 149
 150/-! ## §4. Master Bridge Certificate -/
 151
 152/-- Master certificate for the Higgs–Yukawa bridge. -/
 153structure HiggsYukawaBridgeCert where
 154  /-- THEOREM: every Yukawa is positive for `v > 0`. -/
 155  yukawa_pos      : ∀ s r Z v, 0 < v → 0 < yukawa_SM s r Z v
 156  /-- THEOREM: adjacent-rung scaling by `φ`. -/
 157  yukawa_phi_step : ∀ s r Z v, 0 < v →
 158    yukawa_SM s (r + 1) Z v = phi * yukawa_SM s r Z v
 159  /-- THEOREM: integer-rung scaling by `φ^n`. -/
 160  yukawa_phi_pow  : ∀ s r Z (n : ℕ) v, 0 < v →
 161    yukawa_SM s (r + (n : ℤ)) Z v = phi ^ n * yukawa_SM s r Z v
 162  /-- THEOREM: ratio of Yukawas equals ratio of masses. -/
 163  yukawa_ratio_v_independent :
 164    ∀ s r1 r2 Z v, 0 < v →
 165      yukawa_SM s r1 Z v / yukawa_SM s r2 Z v
 166        = predict_mass s r1 Z / predict_mass s r2 Z
 167

papers checked against this theorem

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