passiveEdgeCount
plain-language theorem explainer
passiveEdgeCount supplies the integer count of passive field edges at D=3, which evaluates to 11. Researchers deriving lepton generation mass ratios cite this count when separating the integrated coupling from the single-direction transition step. The definition is obtained by direct substitution of the dimension constant into the upstream passive_field_edges function.
Claim. Let $D=3$. The passive edge count is defined as $N_p := E(D) - A$, where $E(D)$ is the total number of edges in the recognition cube of dimension $D$ and $A$ is the number of active edges traversed per tick.
background
Recognition events traverse edges of a discrete cube in $D$ spatial dimensions. Passive edges dress the interaction while a single active edge carries the transition. The upstream definition states: Passive (field) edges: total edges minus active edge. These are the edges that dress the interaction. It is given explicitly by passive_field_edges (d) := cube_edges d - active_edges_per_tick.
proof idea
This is a one-line definition that applies the passive_field_edges function to the constant D.
why it matters
This definition supplies the integer 11 that enters the α geometric seed as totalSolidAngle multiplied by passiveEdgeCount. It feeds alphaSeed, generationStepDerived (which equals 11 + 1/(4π)), and the theorem fractional_step_is_forced. In the framework this closes the geometric origin of the fractional step from the same edge counting that forces the fine-structure constant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.