yukawa_SM_pos
plain-language theorem explainer
The declaration establishes that the Yukawa coupling obtained from the Recognition Science mass law is positive whenever the electroweak scale v exceeds zero. It is invoked inside the Higgs-Yukawa bridge certificate and in the conditional extraction of Standard-Model Yukawas. The proof unfolds the coupling definition and chains the known positivity of the square root of two, the mass prediction, their product, and the final division.
Claim. Let $s$ be a sector, $r$ and $Z$ integers, and $v>0$ a real number. The Yukawa coupling defined by $y(s,r,Z,v) := (√2 · m(s,r,Z))/v$, where $m$ denotes the mass predicted by the Recognition Science mass law, satisfies $y(s,r,Z,v)>0$.
background
The Higgs-Yukawa Bridge module expresses every Standard-Model Yukawa coupling as the ratio of an RS-derived fermion mass to the electroweak scale $v$, using the canonical extraction form $y_f = √2 m_f / v$. The mass $m_f$ is supplied by predict_mass, which places each fermion on the phi-ladder according to its sector (Lepton, UpQuark, DownQuark, or Electroweak) and integer rung. This construction ensures that Yukawa values are never fitted independently; they inherit the phi-ladder structure and the single scale $v$ from the mass law.
proof idea
The term proof first unfolds the definition of yukawa_SM to expose the quotient (√2 · predict_mass)/v. It obtains positivity of √2 from Real.sqrt_pos, positivity of the mass from predict_mass_pos, positivity of the numerator by multiplication, and positivity of the quotient by div_pos.
why it matters
The result supplies the positivity component required by higgsYukawaBridgeCert, which assembles the full bridge properties. It supports the conditional theorem yukawa_SM_pos_of_hypothesis that recovers the SM-extracted Yukawa under the normalization hypothesis, and it is used to establish the adjacent-rung ratio theorem yukawa_SM_ratio_adjacent. Within the framework it closes the positivity requirement for the phi-rung scaling that follows from the eight-tick octave and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.