topYukawa
plain-language theorem explainer
The top Yukawa coupling is assigned the exact value 1 in natural units. Physicists deriving the Higgs vacuum expectation value from J-cost minimization across the five electroweak channels cite this assignment to fix the top-loop contribution at unity. The definition is introduced by direct constant assignment with no further computation or hypotheses.
Claim. The top Yukawa coupling is defined by the assignment $y_t = 1$.
background
The module treats the Higgs vacuum expectation value as the recognition minimum of the J-cost ratio across five canonical electroweak breaking channels (top-loop, bottom-loop, tau-loop, W-loop, Z-loop), with $v_H$ near 246 GeV. The top Yukawa is fixed at unity to place the top-loop recognition ratio at the unit value required by the minimum. This setting uses the Recognition Composition Law and J-uniqueness from the forcing chain to constrain the channel contributions.
proof idea
Direct definition that assigns the constant 1 to the real number topYukawa.
why it matters
This definition supplies the unit top Yukawa required by the HiggsVEVCert structure, which certifies both the five-channel count and the top Yukawa condition. It supports the claim that the top-loop recognition ratio sits at unity, consistent with the J-cost minimum for the Higgs VEV. The assignment closes the canonical channel setup before the mass formula and phi-ladder relations are applied downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.