same_ingredients
plain-language theorem explainer
The theorem shows that the solid angle Ω, passive edge count N_p and active edge count N_a underlying the alpha seed definition alphaSeed = Ω N_p are identical to the quantities appearing in the lepton generation step generationStepDerived = N_p + N_a / Ω. Researchers deriving the electron-muon mass ratio from geometric first principles would cite it to establish that the 1/(4π) term shares its origin with the fine-structure constant. The proof is a direct term-mode witness that instantiates the three reals and discharges the two equations by r
Claim. There exist real numbers $Ω$, $N_p$, $N_a$ such that $Ω$ equals the total solid angle, $N_p$ equals the passive edge count, $N_a$ equals the active edge count, the alpha seed equals $Ω · N_p$, and the derived generation step equals $N_p + N_a / Ω$.
background
In this module the total solid angle $Ω$ is the 4π steradians fixed by three-dimensional cube geometry. The passive edge count $N_p$ equals 11 and the active edge count $N_a$ equals 1; both counts are fixed by the same lattice geometry that supplies the ingredients for the fine-structure constant. The alpha seed is the integrated product $Ω N_p$ while the generation step is the differential combination $N_p + N_a / Ω$, exactly as the module doc states: the distinction between integrated coupling and single-direction transition forces the 1/(4π) term.
proof idea
The term proof constructs the witness triple (totalSolidAngle, passiveEdgeCount, activeEdgeCount). The first three conjuncts hold by reflexivity. The alphaSeed equation is discharged by rfl. The generationStepDerived equation is discharged by unfolding the definition of generationStepDerived together with fractionalSolidAngle and applying ring simplification.
why it matters
The result closes the local derivation that the 1/(4π) fractional step and the alpha seed are built from identical geometric primitives (D = 3 solid angle and cube edge counts). It therefore supplies the structural link between the alpha derivation and the lepton generation step inside the Recognition framework. No downstream theorems are recorded, so the declaration functions as a self-contained justification for the differential form used in the electron-to-muon mass ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.