pith. machine review for the scientific record. sign in
theorem proved term proof high

passiveEdgeCount_eq

show as:
view Lean formalization →

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.

claimIn 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

 134theorem passiveEdgeCount_eq : passiveEdgeCount = 11 := passive_edges_at_D3

proof body

Term-mode proof.

 135
 136/-- The number of active edges per tick. -/

depends on (9)

Lean names referenced from this declaration's body.