def
definition
correction_D_half
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity on GitHub at line 65.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
62/-! ## Part 2: The Candidate Correction Terms -/
63
64/-- Candidate 1: D/2 (our claimed formula) -/
65noncomputable def correction_D_half (d : ℕ) : ℝ := (d : ℝ) / 2
66
67/-- Candidate 2: F/4 = (2D)/4 = D/2 (algebraically equivalent!) -/
68noncomputable def correction_F_quarter (d : ℕ) : ℝ := (cube_faces d : ℝ) / 4
69
70/-- Candidate 3: E/8 (edges divided by 8) -/
71noncomputable def correction_E_eighth (d : ℕ) : ℝ := (cube_edges d : ℝ) / 8
72
73/-- Candidate 4: D(D-1)/4 (quadratic) -/
74noncomputable def correction_D_quad1 (d : ℕ) : ℝ := (d : ℝ) * ((d : ℝ) - 1) / 4
75
76/-- Candidate 5: D²/6 (another quadratic) -/
77noncomputable def correction_D_quad2 (d : ℕ) : ℝ := ((d : ℝ) ^ 2) / 6
78
79/-! ## Part 3: All Candidates Equal 1.5 in D=3 -/
80
81theorem D_half_at_3 : correction_D_half 3 = 3/2 := by
82 unfold correction_D_half
83 norm_num
84
85theorem F_quarter_at_3 : correction_F_quarter 3 = 3/2 := by
86 unfold correction_F_quarter
87 simp [cube_faces]
88 norm_num
89
90theorem E_eighth_at_3 : correction_E_eighth 3 = 3/2 := by
91 unfold correction_E_eighth
92 simp [cube_edges]
93 norm_num
94
95theorem D_quad1_at_3 : correction_D_quad1 3 = 3/2 := by