trivialYukawaSpurion
plain-language theorem explainer
The trivial Yukawa spurion is introduced as the leading-order case with no flavor violation, by setting both covariance under flavor transformations and suppression by Yukawa couplings to hold. Model builders working on minimal flavor violation in the Recognition Science mass framework cite it when establishing that the anchor display depends only on gauge charges Z at the universal scale. The construction is a direct record definition with both fields instantiated to true.
Claim. Define the trivial Yukawa spurion by the conditions that it is flavor covariant and that its contribution is Yukawa suppressed.
background
The AnchorPolicy module supplies a Lean interface for single-anchor phenomenology in the mass framework, wiring Constants.phi to RSBridge.Anchor and isolating assumptions on the anchor scale and stability. The YukawaSpurion structure parametrizes flavor breaking for MFV analysis via two fields: flavor covariance under symmetry transformations and suppression proportional to Yukawa couplings. This trivial instance represents the case of no flavor violation at leading order, consistent with the module's treatment of the empirical residue as an RG-transport hypothesis f_i(μ⋆) = gap(ZOf i). Upstream results include the integer charge map Z from Masses.Anchor that assigns values by sector and rational charge Q.
proof idea
Direct record construction that instantiates the two Prop fields of the YukawaSpurion structure to true.
why it matters
This definition supplies the leading-order input to the MFV compatibility theorem mfv_compatible_at_anchor, which states that the anchor display remains flavor-universal when the residue depends only on Z. It closes the flavor-structure compatibility concern raised in the module documentation for the single-anchor RG policy. The construction aligns with Recognition Science landmarks by preserving the Z-based mass ladder and the hypothesis that subleading corrections remain Yukawa-suppressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.