def
definition
generationStepDerived
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.FractionalStepDerivation on GitHub at line 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
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:
171 - 11 passive edges contribute discretely (integer part)
172 - 1 active edge contributes fractionally (1/(4π) of a full sphere)
173
174 This is FORCED by the same geometry that forces 4π in the α seed. -/
175theorem fractional_step_is_forced :
176 generationStepDerived - (passiveEdgeCount : ℝ) = (activeEdgeCount : ℝ) / totalSolidAngle := by
177 unfold generationStepDerived fractionalSolidAngle
178 ring
179
180/-- The relationship between α seed and generation step. -/
181theorem alpha_step_relationship :
182 alphaSeed / generationStepDerived =
183 (totalSolidAngle * passiveEdgeCount) / ((passiveEdgeCount : ℝ) + (activeEdgeCount : ℝ) / totalSolidAngle) := by
184 unfold alphaSeed generationStepDerived fractionalSolidAngle
185 ring