muon_rung
plain-language theorem explainer
The declaration assigns the integer 13 as the rung index of the muon on the Recognition Science phi-ladder. Researchers calibrating the RS mass formula against the muon g-2 anomaly would cite this constant when constructing the counter-term. The definition is a direct constant assignment with no computation or lemmas.
Claim. The rung index for the muon on the $phi$-ladder is defined as the integer $13$.
background
In the EA-001 module the muon g-2 anomaly is resolved by phi-ladder calibration of the RS mass formula. The gap function appears in four upstream definitions: as the product of closure and Fibonacci factors (Gap45.Derivation), as the logarithmic residue $F(Z) = ln(1 + Z/phi)/ln(phi)$ (RSBridge.Anchor and Masses.RSBridge.Anchor), and as the sector-dependent form in AnchorPolicy. These supply the rung offset term rung - 8 + gap(Z) that converts the yardstick into a physical mass.
proof idea
One-line definition that directly assigns the constant 13 to muon_rung.
why it matters
muon_rung supplies the exponent used inside rs_counter_term and thereby feeds the theorems phi_ladder_confirms_muon_mass, rs_counter_positive, and rs_counter_term that certify the EA-001 resolution. It implements the phi-ladder step of the mass formula that connects the T5 J-uniqueness fixed point to the observed muon mass.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.