higgsYukawaBridgeCert
plain-language theorem explainer
This definition assembles the master certificate HiggsYukawaBridgeCert by direct assignment of four component theorems. It certifies that Yukawa couplings y_f = √2 m_f / v, with m_f taken from the phi-ladder mass law, are positive for v > 0, scale by phi under rung increments, obey integer-power scaling, and have v-independent ratios. Standard-model phenomenologists would cite it when confirming that fermion Yukawas require no independent parameters beyond rung assignments. The construction is a one-line bundling of sibling results into the pre
Claim. The certificate asserts: for y_f = √2 m_f / v with m_f the RS mass on the phi-ladder, (i) 0 < y_f whenever v > 0, (ii) y(r+1) = φ y(r), (iii) y(r+n) = φ^n y(r) for n ∈ ℕ, and (iv) y(r1)/y(r2) equals the mass ratio m(r1)/m(r2) independent of v.
background
The module defines the Higgs–Yukawa bridge by expressing every SM Yukawa as y_f = √2 m_f / v, where m_f comes from Masses.MassLaw.predict_mass on the phi-ladder. The phi-rung scaling property is inherited directly: a one-rung increase multiplies the Yukawa by φ. Upstream theorems supply the four required properties. yukawa_SM_pos proves positivity from sqrt(2) > 0 and predict_mass_pos. yukawa_SM_phi_scaling unfolds yukawa_SM and invokes mass_rung_scaling. yukawa_SM_phi_pow_scaling proceeds by induction on n. yukawa_SM_ratio_independent_of_v cancels the common √2 / v factor.
proof idea
The definition is a direct structure constructor. It populates the four fields of HiggsYukawaBridgeCert by naming the sibling theorems: yukawa_pos := yukawa_SM_pos, yukawa_phi_step := yukawa_SM_phi_scaling, yukawa_phi_pow := yukawa_SM_phi_pow_scaling, and yukawa_ratio_v_independent := yukawa_SM_ratio_independent_of_v. No additional tactics or reductions are performed.
why it matters
The certificate is consumed by higgsEFTLowEnergyLimitCert, which bundles it with the Higgs–EFT, electroweak-mass, and observable certificates to certify the low-energy limit. It realizes the module claim that no Yukawa is fitted independently; each is fixed by the fermion’s rung on the phi-ladder and the single scale v. This step closes the Yukawa sector of the Recognition Science Standard-Model bridge and leaves open only the combinatorial derivation of the rung map itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.