passiveEdgeCount_eq
plain-language theorem explainer
The theorem fixes the passive edge count at eleven for the three-dimensional recognition lattice. Lepton mass ratio derivations cite this to anchor the discrete field contribution in the generation step formula. The proof is a direct one-line substitution of the D3-specific passive field edge theorem.
Claim. In the three-dimensional recognition structure the number of passive field edges equals 11.
background
Recognition events occur at discrete ticks, the fundamental RS time quantum. Each tick distinguishes one active edge (the transition) from eleven passive edges that dress the interaction and contribute to the integrated coupling. The module derives the 1/(4π) term in the lepton generation step from the contrast between discrete edge counting and continuous spherical averaging over 4π steradians. Upstream, the passive_edges_at_D3 theorem states that for D=3, passive_field_edges D = 11, obtained via native_decide after the D=3 result from the forcing chain.
proof idea
The proof is a one-line wrapper that applies the passive_edges_at_D3 theorem from the AlphaDerivation module.
why it matters
This equality supplies the fixed passive edge count required by the lepton generation step derivation in the same module, where step_e_mu = E_passive + 1/(4π) - α². It closes the discrete contribution to the fractional solid angle and links directly to the D=3 result (T8) and the structural origin of the 4π factor in the alpha seed. The declaration has no downstream uses recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.