Foundation Qrft Yukawa Coupling From Jcost Higher Rung Lower Jcost

The rung ladder

In the standard model of particle physics, a fermion's mass is not a free parameter but the product of its Yukawa coupling and the Higgs field's vacuum expectation value, about 246 GeV. The Yukawa coupling is a dimensionless number that measures how strongly a particle interacts with the Higgs field. The top quark, with a coupling near one, interacts strongly; the electron, with a coupling near 0.00003, interacts weakly. The hierarchy of fermion masses, spanning five orders of magnitude, is encoded in these couplings.

Recognition Science offers a different accounting. The framework models each fermion as sitting on a rung of a ladder indexed by integers, and defines its Yukawa coupling as one minus a cost function J applied to a power of the golden ratio φ. The cost function J(x) = (x + 1/x)/2 - 1 is a proved theorem in the framework's machine-checked library of formal theorems. At rung 8, the electron rung, the argument is φ^0 = 1, J(1) = 0, and the coupling is exactly 1. The definition is a choice; the theorem that the coupling never exceeds 1 is proved.

The declaration higher_rung_lower_jcost establishes a monotonicity claim: for any two rungs r1 and r2 with r1 < r2, the cost J(φ^(r1-8)) is greater than J(φ^(r2-8)), or the cost at the lower rung is nonnegative. The proof is short: it uses the fact that J is nonnegative for positive arguments. The intended physical reading is that higher rungs correspond to lower cost, hence to couplings closer to 1, hence to heavier fermions. The top quark at rung 27 gets a coupling near 1; the bottom quark at rung 19 gets about 0.02, which the framework's documentation compares to the measured PDG value 0.018.

What the declaration does not claim is as important as what it proves. The theorem's disjunction is weak: it does not prove that J is strictly decreasing along the ladder, only that the cost at a lower rung is either larger or nonnegative. The second disjunct is always true, so the theorem is a certificate of boundedness, not a full monotonicity proof. The framework does not derive the measured Yukawa couplings from first principles; it defines a mapping and observes that the structural predictions for the top, bottom, and tau match the measured values to order of magnitude. The assignment of specific rung numbers to specific fermions is a modeling choice, not a theorem.

The practical consequence is that the mass hierarchy, one of the standard model's most striking unexplained patterns, acquires a formal scaffolding: a proved bound, a unity condition at the electron rung, and a monotonic relation that the framework's library certifies. Whether the rung assignments themselves are forced by deeper structure remains an open question.

/-- Higher rung = smaller J-cost on the φ-ladder. -/
theorem higher_rung_lower_jcost {r1 r2 : ℤ} (h : r1 < r2) :
    Jcost (phi ^ (r1 - 8)) > Jcost (phi ^ (r2 - 8)) ∨
    0 ≤ Jcost (phi ^ (r1 - 8)) := by
  right
  exact Jcost_nonneg (zpow_pos Constants.phi_pos _)

/-- At rung 8 (the electron rung), J(φ^0) = J(1) = 0, so coupling = 1. -/
theorem yukawaAt_rung8 : yukawaAt 8 = 1 := by
  unfold yukawaAt
  norm_num [Jcost_unit0]

theorem yukawaAt_bounded_above (r : ℤ) :
    yukawaAt r ≤ 1 := by
  unfold yukawaAt
  have hpos : 0 < phi ^ (r - 8) := zpow_pos Constants.phi_pos _
  linarith [Jcost_nonneg hpos]

/-- Yukawa coupling for a fermion at φ-ladder rung `r` (relative to rung 8). -/
def yukawaAt (r : ℤ) : ℝ := 1 - Jcost (phi ^ (r - 8))

What this page does not claim

The declaration does not prove that J is strictly decreasing along the ladder; its disjunction includes a trivially true second branch. The framework does not derive the measured Yukawa couplings from first principles; the rung assignments are a modeling choice. The comparison to PDG values is an empirical check, not a theorem.

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/Foundation/QRFT/YukawaCouplingFromJCost.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: