activeEdgeCount_eq
plain-language theorem explainer
The theorem confirms that exactly one active edge is traversed per recognition tick when deriving the lepton generation step. Researchers isolating the differential mass contribution in the electron-muon ratio would cite this when separating active transitions from passive field dressing. The proof is a direct reflexivity reduction on the definition of the active edge count as the constant one.
Claim. The number of active edges traversed per recognition tick equals 1.
background
The module derives the 1/(4π) term in the lepton generation step formula from the distinction between discrete edge counting and continuous spherical averaging. Each recognition tick at a given event features one active edge for the differential transition and eleven passive edges for the integrated coupling. The active edge count is introduced as the natural number equal to the constant representing active edges per tick.
proof idea
The proof is a one-line reflexivity wrapper that applies directly to the definition of the active edge count.
why it matters
This anchors the single active edge's role in the differential contribution to the generation step, which feeds the derived equality for the electron-to-muon mass ratio. It supports the structural separation of the 1/(4π) factor arising from full solid-angle integration over 4π steradians versus the discrete active count. The result closes the active-edge part of the two-formula derivation in the lepton module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.