muon_electron_ratio
plain-language theorem explainer
The theorem fixes the muon-to-electron mass ratio as exactly φ^11 for leptons under the single-anchor RG policy. Researchers mapping lepton hierarchies or muonic atom corrections would cite it when converting rung differences into observed ratios. The proof invokes the anchor_ratio lemma after confirming equal Z assignments for the two fermions and substituting a rung gap of 11.
Claim. Assuming a residue function $f :$ Fermion $→ ℝ → ℝ$ satisfies the display identity at the anchor, the ratio of muon to electron masses at the anchor equals $φ^{11}$.
background
The AnchorPolicy module supplies the single-anchor RG policy for masses, with the residue function $f_i(μ⋆)$ defined as the integrated anomalous dimension $(1/ ln φ) ∫ γ_i(μ') d(ln μ')$ from the anchor scale to the physical mass. The display identity hypothesis equates this residue to the gap function F(Z) = gap(ZOf i). The rung function assigns integer levels on the phi-ladder (r_e = 2, r_μ = 13). Upstream anchor_ratio from RSBridge.Anchor states that equal Z values imply massAtAnchor a / massAtAnchor b = φ^(rung a - rung b).
proof idea
The tactic proof first obtains ZOf Fermion.mu = ZOf Fermion.e by native_decide. It applies the anchor_ratio lemma to this equality. A separate have block computes the rung difference as exactly 11 via simp and norm_num. Substituting the difference into the anchor_ratio result produces the target equality.
why it matters
This supplies the muon-electron factor to lepton_masses_from_ladder, which resolves P-011 by fixing all lepton ratios via phi-ladder spacings (11, 17, 6). It also populates the muon_electron_ratio definition used in ProtonRadius for muonic Bohr radius estimates. The result instantiates the mass formula on the phi-ladder for leptons and closes the flavor compatibility scaffolding noted in the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.