`activeEdgeCount_eq`

proved

show as: view math explainer →

module: IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation
domain: Physics
line: 140 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation on GitHub at line 140.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 137def activeEdgeCount : ℕ := active_edges_per_tick
 138
 139/-- Verify active edge count = 1. -/
 140theorem activeEdgeCount_eq : activeEdgeCount = 1 := rfl
 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. -/
 146noncomputable def alphaSeed : ℝ := totalSolidAngle * passiveEdgeCount
 147
 148/-- Verify α seed = 4π × 11 = geometric_seed. -/
 149theorem alphaSeed_eq : alphaSeed = geometric_seed := by
 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. -/
 155noncomputable def generationStepDerived : ℝ :=
 156  (passiveEdgeCount : ℝ) + (activeEdgeCount : ℝ) * fractionalSolidAngle
 157
 158/-- The generation step equals 11 + 1/(4π). -/
 159theorem generationStepDerived_eq :
 160    generationStepDerived = 11 + 1 / (4 * Real.pi) := by
 161  unfold generationStepDerived passiveEdgeCount activeEdgeCount fractionalSolidAngle totalSolidAngle
 162  simp only [passive_field_edges, cube_edges, active_edges_per_tick, D]
 163  ring
 164
 165/-! ## Part 4: Physical Interpretation -/
 166
 167/-- **Main Theorem**: The 1/(4π) term is the fractional solid angle
 168    contribution of the single active edge during a generation transition.
 169
 170    Physical interpretation:

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.