theorem proved term proof

`alphaSeed_eq`

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

formal statement (Lean)

 149theorem alphaSeed_eq : alphaSeed = geometric_seed := by

proof body

Term-mode proof.

 150  unfold alphaSeed totalSolidAngle passiveEdgeCount geometric_seed geometric_seed_factor
 151  simp only [passive_field_edges, cube_edges, active_edges_per_tick, D]
 152
 153/-- The generation step: DIFFERENTIAL contribution.
 154    This uses division by 4π because we're taking a single-direction step. -/

depends on (11)

Lean names referenced from this declaration's body.

step in IndisputableMonolith.Complexity.CellularAutomata decl_use
active_edges_per_tick in IndisputableMonolith.Constants.AlphaDerivation decl_use
cube_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
geometric_seed in IndisputableMonolith.Constants.AlphaDerivation decl_use
geometric_seed_factor in IndisputableMonolith.Constants.AlphaDerivation decl_use
passive_field_edges in IndisputableMonolith.Constants.AlphaDerivation decl_use
geometric_seed in IndisputableMonolith.Cosmology.CosmologicalConstantDerivation decl_use
alphaSeed in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
passiveEdgeCount in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
totalSolidAngle in IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation decl_use
geometric_seed in IndisputableMonolith.RRF.Foundation.Constants decl_use