theorem
proved
deltaStructural_eq_half_D3
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepDeltaDerivation on GitHub at line 165.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
162 norm_num
163
164/-- In D = 3 specifically, 2^{D-2} = 2^1 = 2, so we get D/2. -/
165theorem deltaStructural_eq_half_D3 : deltaStructural 3 = (3 : ℝ) / 2 := deltaStructural_D3
166
167/-! ## The Face-Vertex Interpretation
168
169**Physical interpretation of the derivation**:
170
171The tau transition is mediated by the faces of the cubic voxel.
172Each face is a 2D object (square in D=3) with V = 4 vertices.
173
174The radiative correction receives a contribution from each face,
175but the contribution is "spread" over the face's vertices.
176
177Contribution per face-vertex pair: 1
178Total contribution: F faces × 1 / V vertices per face = F/V = D/2
179
180This is NOT a fit — it follows from the face geometry.
181-/
182
183/-- The face-vertex ratio F/V equals D/2 when V = 4 (the 2D case).
184 Verified specifically for D = 3. -/
185theorem faceVertexRatio_D3 :
186 (faceCount 3 : ℝ) / 4 = (3 : ℝ) / 2 := by
187 unfold faceCount
188 norm_num
189
190/-- At D = 3, the face vertex count is 4, confirming the 2D structure. -/
191theorem D3_has_2D_faces : faceVertexCount 3 = 4 := faceVertexCount_D3
192
193/-! ## The Discrete/Continuous Duality
194
195This section formalizes why F/V is the correct formula, by analogy