alphaSeed
plain-language theorem explainer
alphaSeed defines the integrated geometric seed for the fine-structure constant as the product of the total solid angle in D=3 and the passive edge count of 11. Researchers deriving lepton generation steps from recognition edge counting cite this when separating integrated coupling from differential mass ratios. The definition is a direct multiplication that reproduces the 4π·11 value required by the alpha geometric seed.
Claim. $α_{seed} := 4π × N_p$ where $N_p = 11$ counts the passive edges in the D=3 recognition lattice and $4π$ is the total solid angle of the unit 2-sphere.
background
The module derives the 1/(4π) term in the lepton generation step from the distinction between discrete edge counting and continuous spherical averaging. totalSolidAngle is defined as 4 * Real.pi, the surface area of the unit 2-sphere in ℝ³. passiveEdgeCount is defined as passive_field_edges D and equals 11 for D=3 cube geometry. The upstream geometric_seed from AlphaDerivation states: 'The full geometric seed: Ω(∂Q₃) × E_passive. Both factors derive from Q₃ geometry: 4π = Gauss-Bonnet total curvature of ∂Q₃, 11 = cube edges − 1 active edge.'
proof idea
One-line definition that multiplies totalSolidAngle by passiveEdgeCount. No tactics or lemmas are applied inside the body; the equality to geometric_seed is established in the downstream theorem alphaSeed_eq by unfolding and simp on passive_field_edges, cube_edges, and D.
why it matters
This definition supplies the integrated coupling factor that feeds alphaSeed_eq, alpha_step_relationship, and same_ingredients. It fills the integrated half of the generation-step derivation, where alphaSeed = 4π × 11 contrasts with the differential step that divides by 4π. The construction rests on the D=3 geometry fixed by T8 and supplies the α seed that appears inside the (137.030, 137.039) band.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.