def definition def or abbrev

`activeEdgeCount`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

 137def activeEdgeCount : ℕ := active_edges_per_tick

Definition body.

 138
 139/-- Verify active edge count = 1. -/

From the project-wide theorem graph. These declarations reference this one in their body.

activeEdgeCount_eq in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
alpha_step_relationship in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
fractional_step_is_forced in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
generationStepDerived in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
generationStepDerived_eq in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
same_ingredients in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use

Lean names referenced from this declaration's body.

active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use