alpha_step_relationship
plain-language theorem explainer
The theorem establishes the algebraic identity relating the alpha seed (integrated coupling from solid-angle times passive edges) to the derived generation step (differential transition) in the lepton mass-ratio formula. Physicists deriving structural particle masses from recognition geometry would cite it to separate the 4π-integrated contribution from the active-edge differential. The proof reduces to unfolding the three definitions followed by ring normalization.
Claim. Let $a$ be the alpha seed, $s$ the derived generation step, $Ω$ the total solid angle, $n_p$ the passive edge count, and $n_a$ the active edge count. Then $a/s = (Ω · n_p) / (n_p + n_a/Ω)$.
background
The module derives the 1/(4π) term in the electron-to-muon step from the distinction between integrated coupling and differential transition in a recognition event. Passive edges (11) contribute to the alpha seed via full solid-angle integration (4π × 11), while the single active edge supplies the differential contribution. totalSolidAngle, passiveEdgeCount, and activeEdgeCount are defined in sibling declarations; alphaSeed and generationStepDerived are the integrated and differential combinations respectively. Upstream results supply the underlying cellular-automaton step rule and simplicial-continuum bridge that justify treating edges as discrete recognition carriers.
proof idea
One-line wrapper that unfolds alphaSeed, generationStepDerived, and fractionalSolidAngle then applies the ring tactic to normalize the resulting rational expression.
why it matters
The identity confirms that the fractional step in lepton generations follows directly from the same geometric ingredients used for alpha (D=3 solid angle, 11 passive edges from cube geometry, one active edge from atomicity). It closes the structural part of the lepton-generation derivation without introducing fitted parameters and supports the Recognition Science forcing chain at T8 (D=3) and the alpha band. No downstream theorems yet consume it; the declaration therefore functions as a self-contained verification step inside the module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.