o4_slot_forcing_certificate
plain-language theorem explainer
The O4 slot forcing certificate fixes the ledger fraction at exactly 29/44, sets the muon-tau step to the geometric difference 2D minus a linear alpha term built from wallpaper groups, and places the electron-muon step at E_passive plus 1/(4 pi) minus the second-order correction. Lepton-mass modelers in Recognition Science cite it as the canonical coefficient closure for the one-parameter J-cost families. The proof is a term-mode refinement that applies the pre-established ledger-fraction equality, splits the electron-muon channel, and simp-rew
Claim. The O4 closure certificate asserts that the ledger fraction equals $29/44$, the muon-tau step equals $2D - ((2·17 + D)/2)·α$, and the electron-muon step equals $E_ {passive} + 1/(4π) - c^{(2)}$, where $D$ is spatial dimension, $α$ the fine-structure constant, $E_{passive}$ the passive edge count, and $c^{(2)}$ the order-2 correction term.
background
The module supplies the Lean closure package for O4 perturbative coefficients inside the mass-layer J-cost bridge. J-cost is the functional J(x) = (x + x^{-1})/2 - 1 that appears in the Recognition forcing chain; defectDist measures deviations on the phi-ladder; the one-parameter families are the primary constrained expansions used for lepton steps. Local setting is the certification of canonical integer/rational slots for the lepton chain after the Jcost(1+α) channel form and the α² + 12α³ radiative decomposition have been introduced. Upstream, alpha is the fine-structure constant 1/alphaInv; cube_faces(d) := 2d counts hypercube faces; wallpaper_groups := 17 is the Fedorov crystallographic count; E_passive abbreviates passive_field_edges(D) = 11.
proof idea
The proof is a term-mode refinement. It directly supplies the pre-proved ledger_fraction_eq_29_over_44 for the first conjunct, invokes step_e_mu_channel_split for the electron-muon conjunct, and uses simp [step_mu_tau] to discharge the middle geometric identity.
why it matters
The declaration supplies the final O4 coefficient-forcing certificate for the lepton chain inside the J-cost perturbation bridge. It realizes the canonical slots required by the mass-topology counts and the ledger-fraction lemmas that precede it. In the Recognition framework it instantiates T5 J-uniqueness and the eight-tick octave constraints on the phi-ladder steps for D = 3; no open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.