fractional_step_is_forced
plain-language theorem explainer
The theorem shows that the derived generation step for lepton transitions equals the passive edge count plus the active edge count divided by the total solid angle. Physicists deriving lepton mass ratios from the recognition framework cite this result to justify the 1/(4π) term. The proof is a direct algebraic simplification obtained by unfolding the definitions of the generation step and the fractional solid angle.
Claim. $G - p = a / Ω$, where $G$ is the derived generation step, $p$ the passive edge count, $a$ the active edge count, and $Ω$ the total solid angle.
background
The module derives the 1/(4π) fractional contribution to the lepton generation step from the geometry of recognition events. In each tick, 11 passive edges integrate over the full sphere to set the coupling while the single active edge contributes only its directional fraction. generationStepDerived is defined as passiveEdgeCount plus activeEdgeCount times fractionalSolidAngle, with fractionalSolidAngle equal to one over totalSolidAngle. The upstream cellular automaton step applies local rules to produce the successor tape.
proof idea
The proof unfolds generationStepDerived and fractionalSolidAngle, then invokes the ring tactic to cancel terms and obtain the equality. It depends on the definitions of activeEdgeCount, passiveEdgeCount, and totalSolidAngle from the same module.
why it matters
This result grounds the fractional step in the lepton generations module and supports the alpha seed derivation. It realizes the geometric forcing of 4π from the D=3 spatial structure. The parent result is the alpha seed equality in the sibling module, as noted in the module doc-comment that the term is forced by the same geometry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.