theorem proved term proof

`activeEdgeCount_eq`

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

formal statement (Lean)

 140theorem activeEdgeCount_eq : activeEdgeCount = 1 := rfl

proof body

Term-mode proof.

 141
 142/-! ## Part 3: The Two Formulas -/
 143
 144/-- The α geometric seed: INTEGRATED coupling.
 145    This uses multiplication by 4π because we integrate over all directions. -/

depends on (5)

Lean names referenced from this declaration's body.

all in IndisputableMonolith.Aesthetics.NarrativeGeodesic decl_use
all in IndisputableMonolith.Anthropology.KinshipGraphCohomology decl_use
all in IndisputableMonolith.Engineering.AsteroidOreSpectroscopy decl_use
all in IndisputableMonolith.Musicology.ModalPreferenceFromPhi decl_use
activeEdgeCount in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use