alphaSeed_eq
plain-language theorem explainer
The theorem verifies that the alpha seed used in lepton generation steps equals the geometric seed, which evaluates to 4π times 11 from 3-cube edge counting. Researchers deriving mass ratios between lepton generations in the recognition framework cite this to anchor the fractional 1/(4π) term. The proof is a one-line wrapper that unfolds the seed definitions and simplifies via the passive-edge and cube-edge lemmas.
Claim. $α_{seed} = Ω(∂Q_3) × E_{passive} = 4π × 11$, where the geometric seed is the product of the solid angle of the 3-cube boundary and the count of passive field edges.
background
The module derives the 1/(4π) fractional step in the lepton generation formula step_e_mu = E_passive + 1/(4π) - α² from the distinction between integrated coupling (alpha formula) and differential transition (mass step). Passive field edges are defined as cube_edges(d) minus active_edges_per_tick, with active_edges_per_tick fixed at 1 and cube_edges(d) = d · 2^(d-1). For D=3 this yields 11 passive edges. The geometric seed is then solid_angle_Q3 times the passive edge count, giving the full 4π·11 factor that appears in the alpha seed.
proof idea
The term proof unfolds alphaSeed, totalSolidAngle, passiveEdgeCount, geometric_seed and geometric_seed_factor, then applies simp using the lemmas passive_field_edges, cube_edges, active_edges_per_tick and the constant D. This directly reduces both sides to the common expression 4π·11.
why it matters
The equality supplies the seed value required by the downstream generationStepDerived theorem in the same module, closing the structural derivation of the differential lepton step. It rests on the geometric_seed definition from AlphaDerivation, which encodes the T8 choice of D=3 and the passive-edge count of 11. The result anchors the 1/(4π) term without invoking the recognition composition law or J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.