emu_ingredients
plain-language theorem explainer
The declaration establishes that passive field edges in dimension D equal eleven, that the integer four satisfies four times one equals four, and that D equals three. A physicist modeling lepton mass corrections would cite this to fix the geometric inputs for the electron-to-muon transition formula. The proof is a one-line wrapper that applies native decision procedures to discharge the three conjuncts simultaneously.
Claim. Let $D$ denote spatial dimension. Then passive_field_edges$(D)=11$, $4·1=4$, and $D=3$.
background
The module treats sub-leading corrections to lepton mass steps beyond integer cube counts. For the e→μ transition the correction takes the form E_pass + 1/(4π) − α², where E_pass is the integer part supplied by passive_field_edges. Upstream, passive_field_edges(d) is defined as cube_edges(d) minus active_edges_per_tick; its value is eleven when d equals three. The module also records that the spherical factor 1/(4π) is the unique solid-angle normalization on the two-sphere in three dimensions, while the wallpaper coupling W equals seventeen.
proof idea
The proof is a term-mode one-line wrapper. It applies refine to produce a triple of goals and then discharges each goal by native_decide, which evaluates the three equalities directly.
why it matters
The result supplies the concrete geometric constants required by the e→μ correction formula in the lepton mass ladder. It closes the structural constraint that the integer part must be eleven and that the spherical term must be normalized by 4π in D=3, consistent with the eight-tick octave and the forcing of three spatial dimensions. No downstream theorems are listed, so the lemma functions as a verified input rather than an intermediate step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.