No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
131def passiveEdgeCount : ℕ := passive_field_edges D
proof body
Definition body.
132
133/-- Verify passive edge count = 11. -/
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
alphaSeed
in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation
decl_use
-
alphaSeed_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
-
passiveEdgeCount_eq
in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation
decl_use
-
same_ingredients
in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation
decl_use
depends on (1)
Lean names referenced from this declaration's body.