mfv_compatible_at_anchor
plain-language theorem explainer
The theorem shows that under the minimal flavor violation hypothesis the residue function at the anchor scale depends only on gauge charge Z, so the leading display is flavor universal. Particle physicists modeling fermion masses on the phi ladder would cite it to justify Z-only leading terms before Yukawa corrections. The proof is a direct term-mode construction that specializes the given Z-only hypothesis at muStar and instantiates the trivial Yukawa spurion for the subleading part.
Claim. Let $f_ {res} : Fermion → ℝ → ℝ$ satisfy $Z(f)=Z(g) ⇒ f_{res}(f,μ)=f_{res}(g,μ)$ for all μ. Then for every anchor specification $A$ with equal-weight condition, (i) $Z(f)=Z(g)$ implies $f_{res}(f,μ_⋆(A))=f_{res}(g,μ_⋆(A))$, and (ii) for every fermion there exists a Yukawa spurion that is flavor covariant and Yukawa suppressed.
background
AnchorSpec encodes the universal anchor scale μ⋆ together with the equal-weight condition that abstracts PMS/BLM mass-free stationarity and motif equal weights at μ⋆. YukawaSpurion is the formal structure parametrizing flavor breaking, with fields for flavor covariance and Yukawa suppression. The module sets the integrated RG residue $f_i(μ_⋆) := (1/ln φ) ∫{ln μ⋆}^{ln m_phys} γ_i(μ') d(ln μ')$ and hypothesizes it equals the display function gap(ZOf i). Upstream results supply the RRF local recognition field and the gap function used in the display.
proof idea
The term proof introduces the anchor A and discards the equal-weight hypothesis, then builds the conjunction. The first conjunct is obtained by direct application of the MFV hypothesis specialized at A.muStar. The second conjunct is witnessed by the trivial Yukawa spurion whose two properties hold by definition, closed with simp.
why it matters
The result secures flavor universality for the leading anchor display in the single-anchor RG policy, supporting the phi-ladder mass formula where primary recognition depends only on Z. It directly addresses the flavor-structure compatibility concern raised in the module, closing one piece of the stability and flavor scaffolding. It touches the open question of explicit RG transport kernels left to external tools.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.