lepton_integer_slot_iff_bundle_no_hk
plain-language theorem explainer
The theorem packages two lepton-step equivalences into one bundled iff under the given perturbative forms for e-mu and mu-tau transitions. Recognition Science researchers closing O4 mass coefficients would cite it to confirm forced integer slots without hyperkähler terms. The proof is a direct term-mode conjunction of two specialized denominator-matching lemmas.
Claim. Under the assumptions that the electron-muon step equals the passive energy plus $1/(k_e π)$ minus $q$ times the second-order correction, with $n ≤ D$, and the muon-tau step equals $2D$ minus $((2·17 + n)/k_μ) α$, it holds that $(k_e = 4 ↔ q = 1) ∧ (k_μ = 2 ↔ n = D)$.
background
The JCostPerturbation module supplies the O4 perturbative bridge for lepton masses, certifying the J-cost(1+α) channel form and the explicit α² + 12α³ decomposition. Key constants are α (fine-structure, defined as 1/α_inv), cube_faces D := 2D (hypercube faces), and wallpaper_groups := 17 (Fedorov crystallographic count). The local setting is the mass-layer closure that ties canonical arithmetic objects to the lepton-step definitions via positivity-free integer-family equivalences.
proof idea
Term-mode proof via refine that splits the target conjunction. The left conjunct is discharged by exact application of step_e_mu_denominator_iff_quadratic_scale_no_hk to the e-mu hypothesis. The right conjunct is discharged by exact application of step_mu_tau_denominator_iff_numerator_under_dim_bound_no_hk to the dimension bound and mu-tau hypothesis.
why it matters
This bundles the e→μ mixed-slot and μ→τ denominator equivalences to close the O4 coefficient forcing in the J-cost perturbation path. It feeds the canonical arithmetic and alpha-derivation chain while supporting the phi-ladder mass formulas by confirming the forced slots k_e=4 and k_mu=2 under the dimensional bound. No downstream uses are recorded yet; it serves as an internal packaging step for the lepton integer family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.