step_e_mu_invpi_denominator_forced
plain-language theorem explainer
Matching the canonical e to μ step to the one-parameter family E_passive + 1/(k π) minus second-order correction forces the integer k to equal 4. Researchers closing lepton mass ratios via J-cost perturbations in the Recognition Science framework cite this to fix the denominator coefficient. The proof obtains the explicit 4π form from the channel-split lemma then cancels the common π factor by linear arithmetic on the two expressions for step_e_mu.
Claim. If the muon-electron step satisfies $step_{eμ} = E_{passive} + 1/(k π) - C_2$ for positive integer $k$, where $C_2$ denotes the second-order correction, then $k=4$.
background
The JCostPerturbation module supplies the O4 perturbative closure for mass-layer steps, linking the J-cost channel form to canonical lepton definitions. Here step_e_mu is the energy difference between muon and electron on the phi-ladder, E_passive is the zeroth-order passive-edge term, and correction_order_2 is the explicit α² term in the one-parameter family. The local setting is the mass-layer bridge that certifies the Jcost(1+α) perturbative channel and the α² + 12α³ radiative decomposition.
proof idea
The tactic proof first applies step_e_mu_channel_split to obtain the canonical expression with denominator 4π. Linear arithmetic equates the two fractional terms. Positivity of k and non-vanishing of the denominators are derived, after which nlinarith yields kπ = 4π. The common π factor is canceled by mul_right_cancel and Nat.cast injectivity.
why it matters
This result pins the inverse-π denominator for the e→μ step and feeds directly into step_e_mu_full_family_forced_from_passive_term. It completes one coefficient-forcing step in the O4 closure of the Recognition Science mass formulas, consistent with the phi-ladder rung structure and the eight-tick octave. It touches the open question of whether higher-order radiative terms remain compatible with the same denominator forcing.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.