rung_exponent
plain-language theorem explainer
The rung_exponent definition supplies integer steps for the phi-ladder mass surrogate restricted to charged leptons. It returns 11 for the mu_e name, 6 for tau_mu, and 0 for every other string. Modelers working on lepton mass consistency cite the placeholder when they invoke the ladder bound against imported measurements. The body is a direct conditional that hard-codes the two surrogate cases.
Claim. The function $e : String → ℤ$ satisfies $e(``mu_e'') = 11$, $e(``tau_mu'') = 6$, and $e(n) = 0$ for every other string $n$.
background
The module models a charged-lepton ladder surrogate in which masses sit on the phi-ladder. The rung_exponent supplies the integer differences that appear inside the mass formula yardstick · φ^(rung − 8 + gap(Z)). mu_e and tau_mu label the two surrogate pairs whose exponents are fixed by the paper placeholder; all other names default to rung 0.
proof idea
The definition is a nested if-then-else expression on the input string that returns the two hard-coded integers and defaults to zero.
why it matters
The definition is required by mass_ladder_assumption, which asserts that every imported measurement satisfies |m.value − φ^rung_exponent(m.name)| ≤ m.error, and by mass_ladder_matches_pdg. It therefore supplies the concrete rungs for the charged-lepton sector of the phi-ladder formula that descends from the self-similar fixed point phi (T6). The placeholder status leaves open a future derivation of these specific exponents from J-uniqueness or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.