generationStepDerived_eq
plain-language theorem explainer
Generation step derived equals eleven plus one over four pi. Lepton mass modelers cite this for the fractional contribution in generation transitions. The equality follows from unfolding edge counts and solid angle fractions then ring simplification.
Claim. The lepton generation step equals $11 + 1/(4π)$.
background
In the recognition framework, interactions occur via edges on a D-hypercube with D fixed at 3. Cube edges total D times 2 to the D-1, yielding 12 for D=3. One edge is active per tick while the remaining 11 are passive field edges that dress the interaction. The fractional solid angle of the active edge is normalized to 1 over 4π against the full sphere surface. This module isolates the differential contribution of the active edge for mass steps, distinct from the integrated 4π times 11 factor used in the alpha seed.
proof idea
The proof is a term-mode reduction. It unfolds generationStepDerived together with passiveEdgeCount, activeEdgeCount, fractionalSolidAngle, and totalSolidAngle. It then simplifies using the explicit constants passive_field_edges, cube_edges, active_edges_per_tick, and D, followed by ring normalization to reach the target equality.
why it matters
This supplies the explicit fractional step value required by the lepton generation formula in the module. It rests on the same geometry that forces the 4π factor in the alpha derivation, where the 11 passive edges integrate over the full sphere. The result closes the structural account of the 1/(4π) term as a direct consequence of active versus passive edge counting under D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.