def
definition
passiveEdgeCount
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation on GitHub at line 131.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
128/-! ## Part 2: Edge Contributions -/
129
130/-- The number of passive edges in D=3. -/
131def passiveEdgeCount : ℕ := passive_field_edges D
132
133/-- Verify passive edge count = 11. -/
134theorem passiveEdgeCount_eq : passiveEdgeCount = 11 := passive_edges_at_D3
135
136/-- The number of active edges per tick. -/
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