activeEdgeCount
plain-language theorem explainer
activeEdgeCount sets the number of active edges traversed per atomic tick to exactly one. Physicists deriving lepton generation mass ratios reference it when isolating the differential transition term from the integrated coupling in the alpha formula. The definition is a direct one-line re-export of the upstream constant active_edges_per_tick.
Claim. Let $N_a$ be the number of active edges per recognition tick. Then $N_a = 1$.
background
In the Recognition Science framework each atomic tick traverses exactly one active edge transition by the T2 atomicity rule, while 11 passive edges dress the interaction from cube geometry. The module derives the 1/(4π) fractional step by contrasting discrete edge counting with continuous spherical averaging over the 4π steradians fixed by D=3. The upstream result states: 'Active edges per atomic tick (one edge transition per tick by T2).'
proof idea
One-line wrapper that directly references the upstream constant active_edges_per_tick.
why it matters
This supplies the single active edge that enters generationStepDerived and feeds the main theorem fractional_step_is_forced, which isolates the 1/(4π) term as the fractional solid angle contribution of the active edge. The same three ingredients (4π from D=3, 11 passive edges, 1 active edge) appear in both the α seed (integrated) and the step (differential), closing the structural account of the electron-to-muon mass ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.