YukawaSpurion
plain-language theorem explainer
YukawaSpurion supplies a structure that parametrizes flavor breaking for MFV checks inside the single-anchor RG policy. Model builders verifying that subleading flavor effects stay Yukawa-suppressed at the universal anchor scale would cite this definition. It is introduced directly as a structure with two propositional fields and no further reduction steps.
Claim. A Yukawa spurion is a formal object that satisfies flavor covariance (transforms properly under flavor symmetry) and Yukawa suppression (its contribution is proportional to the Yukawa couplings).
background
The declaration lives in the Single-Anchor RG Policy module, whose purpose is to give a precise Lean surface for single-anchor phenomenology in the mass framework while wiring to the phi constant and RSBridge.Anchor infrastructure. It isolates assumptions about the anchor scale and stability so that downstream modules can depend on a clean interface. The module doc states that a spurion is a formal field that parametrizes flavor breaking and that the integrated RG residue is represented as a hypothesis of the form f_i(μ⋆) = F(Z_i).
proof idea
The declaration is a structure definition. It directly encodes the two required properties as fields of type Prop without invoking lemmas or performing reductions.
why it matters
This structure is used by the MFV compatibility theorem to verify that the anchor display remains flavor-universal at leading order, with subleading corrections Yukawa-suppressed. It addresses the flavor-structure compatibility concern listed in the module purpose and supports the single-anchor phenomenology that reuses gap(Z) as the display function. In the broader Recognition framework it connects to the empirical residue transport hypothesis and the requirement that flavor breaking be controlled by Standard Model Yukawa matrices.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.