Standard Model Higgs Yukawa Bridge

The Yukawa bridge

In the Standard Model of particle physics, the Yukawa coupling y_f measures how strongly a fermion (an electron, a quark, a neutrino) interacts with the Higgs field. It is not a free parameter in the usual sense: experimentalists extract it from the measured fermion mass m_f and the electroweak scale v (about 246 GeV, the vacuum expectation value of the Higgs field) using the convention y_f = √2 · m_f / v. The top quark, for instance, has a Yukawa coupling near 1, while the electron's is about 0.00003. These numbers span five orders of magnitude, and the Standard Model offers no explanation for their pattern.

Recognition Science (RS) proposes that the pattern is not arbitrary. Its core claim is that reality keeps a discrete ledger, a record of recognition events, and that the cost of each recognition is forced by a proved uniqueness theorem. From that theorem, a chain of results derives the golden ratio φ = (1 + √5)/2 ≈ 1.618 as the unique self-similar scaling, and then places particle masses on a ladder where each rung multiplies the previous mass by φ. The Higgs–Yukawa bridge applies this ladder to the Yukawa coupling: it defines y_f exactly as the Standard Model does, but with the mass supplied by the RS mass law rather than by measurement.

What the bridge establishes, in machine-checked form, is that this definition inherits the ladder's structure. Four theorems hold for any fermion sector, any rung, and any positive electroweak scale v. First, the Yukawa coupling is always positive. Second, moving up one rung on the mass ladder multiplies the coupling by exactly φ. Third, moving up n rungs multiplies it by φⁿ. Fourth, the ratio of two Yukawa couplings for the same fermion species equals the ratio of their masses, because the factor √2 and the scale v cancel out. These are not approximations; they are exact identities in the framework's formal library.

In Recognition Science, the bridge establishes that no Yukawa coupling is fit independently. Every Yukawa is a function of the fermion's rung on the φ-ladder and of the electroweak scale v, with the Standard Model extraction convention translated into the same ladder structure. The framework does not yet derive which rung each Standard Model fermion occupies; that mapping from cube combinatorics remains an open target. And the identification of the RS Yukawa with the Standard Model value requires the same normalization hypothesis for v that the Standard Model extraction uses. What the bridge does establish is the scaling law: generation jumps are φ^Δr for the integer rung difference Δr, not φ¹ between adjacent Standard Model generations.

The practical consequence is a testable prediction. If the rung map is ever derived, the full Yukawa matrix of the Standard Model would follow from one scale and one ladder, with no free couplings. The bridge itself does not yet deliver that map, but it guarantees that whatever map the combinatorics produces will obey the golden scaling law. That is a constraint the Standard Model does not provide, and it is the bridge's plain-language achievement.

/-- Standard-Model Yukawa extraction convention:

    `y_f = √2 · m_f / v`

    where `m_f = predict_mass sector rung Z` is the φ-ladder mass. -/
def yukawa_SM (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) : ℝ :=
  Real.sqrt 2 * predict_mass sector rung Z / v

/-- Yukawa couplings are positive for `v > 0`. -/
theorem yukawa_SM_pos
    (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) (hv : 0 < v) :
    0 < yukawa_SM sector rung Z v := by
  unfold yukawa_SM
  have hsqrt2 : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  have hm : 0 < predict_mass sector rung Z := predict_mass_pos sector rung Z
  have hnum : 0 < Real.sqrt 2 * predict_mass sector rung Z := mul_pos hsqrt2 hm
  exact div_pos hnum hv

/-- φ-rung scaling: increasing rung by 1 multiplies the Yukawa by `φ`. -/
theorem yukawa_SM_phi_scaling
    (sector : Anchor.Sector) (rung Z : ℤ) (v : ℝ) (hv : 0 < v) :
    yukawa_SM sector (rung + 1) Z v = phi * yukawa_SM sector rung Z v := by
  unfold yukawa_SM
  have hscale : predict_mass sector (rung + 1) Z = phi * predict_mass sector rung Z :=
    mass_rung_scaling sector rung Z
  have hv_ne : v ≠ 0 := ne_of_gt hv
  rw [hscale]
  field_simp

/-- The Yukawa scaling under an integer rung difference `Δr ≥ 0`:

    y_f(rung + n) = φ^n · y_f(rung). -/
theorem yukawa_SM_phi_pow_scaling
    (sector : Anchor.Sector) (rung Z : ℤ) (n : ℕ) (v : ℝ) (hv : 0 < v) :
    yukawa_SM sector (rung + (n : ℤ)) Z v
      = phi ^ n * yukawa_SM sector rung Z v := by
  induction n with
  | zero =>
      simp [yukawa_SM]
  | succ k ih =>
      have h_one_step :
          yukawa_SM sector (rung + ((k : ℤ) + 1)) Z v
            = phi * yukawa_SM sector (rung + (k : ℤ)) Z v := by
        have := yukawa_SM_phi_scaling sector (rung + (k : ℤ)) Z v hv
        simpa [add_assoc] using this
      have hcast : (rung + (((k + 1 : ℕ) : ℤ))) = (rung + ((k : ℤ) + 1)) := by
        push_cast
        ring
      rw [hcast, h_one_step, ih]
      ring

/-- The ratio of two Yukawas (same sector, same charge) equals the ratio
    of their masses; the `v`-dependence cancels. -/
theorem yukawa_SM_ratio_independent_of_v
    (sector : Anchor.Sector) (rung1 rung2 Z : ℤ) (v : ℝ) (hv : 0 < v) :
    yukawa_SM sector rung1 Z v / yukawa_SM sector rung2 Z v
      = predict_mass sector rung1 Z / predict_mass sector rung2 Z := by
  unfold yukawa_SM
  have hsqrt2_pos : 0 < Real.sqrt 2 := Real.sqrt_pos.mpr (by norm_num : (0 : ℝ) < 2)
  have hsqrt2_ne : Real.sqrt 2 ≠ 0 := ne_of_gt hsqrt2_pos
  have hv_ne : v ≠ 0 := ne_of_gt hv
  have hm2_pos : 0 < predict_mass sector rung2 Z := predict_mass_pos sector rung2 Z
  have hm2_ne : predict_mass sector rung2 Z ≠ 0 := ne_of_gt hm2_pos
  field_simp

What this page does not claim

The bridge does not derive which rung each Standard Model fermion occupies. The identification of the RS Yukawa with the Standard Model value is conditional on the same v normalization hypothesis. The framework does not claim to explain why the electroweak scale v itself takes its measured value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/StandardModel/HiggsYukawaBridge.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: