lepton_real_scale_iff_bundle_no_hc_pos
plain-language theorem explainer
The theorem packages the canonical real-scale equivalences for the electron-muon and muon-tau steps into one positivity-free iff statement. Mass-layer modelers cite it when closing O4 perturbative coefficients for lepton sectors under J-cost forms. The proof is a one-line wrapper that invokes the separate e-mu passive-term lemma and mu-tau face-count lemma.
Claim. Let $s, c_e, f, c_μ ∈ ℝ$. Suppose the electron-muon step satisfies step_{eμ} = s + 1/(c_e π) − correction^{(2)} and the muon-tau step satisfies step_{μτ} = f − ((2·17 + 3)α / c_μ). Then (c_e = 4 ↔ s = E_passive) ∧ (c_μ = 2 ↔ f = 6).
background
The J-cost perturbation module expresses lepton steps in numerator-offset form with α corrections. Wallpaper groups equals the crystallographic constant 17; D is the spatial dimension 3; alpha is the fine-structure constant 1/α_inv. E_passive is the passive energy anchor term. The local setting certifies the Jcost(1+α) channel and zeroth-order geometric evaluations without positivity hypotheses. Upstream, the canonical arithmetic object supplies realization-independent Peano structure while magnitude-of-mismatch forces single-valued symmetry comparisons.
proof idea
The proof refines the conjunction into two goals. It applies the exact lemma step_e_mu_scale_iff_passive_term_no_hc_pos to the first hypothesis and step_mu_tau_scale_iff_face_count_no_hc_pos to the second hypothesis. No additional tactics or reductions are required.
why it matters
This declaration closes the cross-sector packaging for lepton real scales inside the O4 perturbative closure. It supports sibling ledger-fraction and mass-topology derivations. It realizes canonical matching forms for the phi-ladder mass formula, tying to the eight-tick octave and D=3 from the forcing chain T0-T8.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.