step_e_mu_passive_term_forced
plain-language theorem explainer
The theorem forces the leading coefficient s in the electron-muon step to equal the passive edge count when the step is written with a fixed inverse-pi term and quadratic correction. Researchers modeling lepton mass hierarchies via J-cost perturbations cite it to anchor the geometric zeroth-order term. The proof is a one-line wrapper that invokes the channel-split identity and applies linear arithmetic to equate the two expressions for the step.
Claim. If the electron-to-muon mass step satisfies $step_{eμ} = s + 1/(4π) - δ^{(2)}$, then $s = E_{passive}$, where $E_{passive}$ is the passive field edge count and $δ^{(2)}$ denotes the order-two correction.
background
The module supplies the Lean closure for O4 perturbative forcing in the mass layer, linking J-cost expansions to canonical lepton steps. The electron-to-muon step decomposes into a passive-edge term, the fixed geometric contribution 1/(4π), and the quadratic correction term. E_passive is the passive field edge count, defined as passive_field_edges D and equal to 11 in three dimensions.
proof idea
The proof is a one-line wrapper. It calls step_e_mu_channel_split to obtain the canonical decomposition step_e_mu = E_passive + 1/(4π) - correction_order_2, then applies linarith to the hypothesis and this identity to conclude s equals E_passive.
why it matters
The result completes the forcing of the zeroth-order passive term inside the J-cost perturbation bridge for the e-to-μ transition. It supports the mass-topology correction lemmas and the lepton-generation definitions by confirming geometric anchoring of the leading coefficient. In the Recognition framework it contributes to the O4 coefficient-forcing package that ties perturbative channels to the phi-ladder mass formulas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.