theorem
proved
E_eighth_not_axisAdditive
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Physics.LeptonGenerations.TauStepExclusivity on GitHub at line 197.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
194/-! ## Part 6: Excluding Common Alternatives (they violate axis additivity) -/
195
196/-- E/8 is not axis-additive (witness: 2+2). -/
197theorem E_eighth_not_axisAdditive : ¬ AxisAdditive correction_E_eighth := by
198 intro h
199 rcases h with ⟨h0, hadd⟩
200 have h22 : correction_E_eighth (2 + 2) = correction_E_eighth 2 + correction_E_eighth 2 := hadd 2 2
201 -- compute both sides
202 unfold correction_E_eighth at h22
203 simp [cube_edges] at h22
204 -- LHS = 4, RHS = 1
205 norm_num at h22
206
207/-- D(D-1)/4 is not axis-additive (witness: 1+1). -/
208theorem D_quad1_not_axisAdditive : ¬ AxisAdditive correction_D_quad1 := by
209 intro h
210 rcases h with ⟨h0, hadd⟩
211 have h11 : correction_D_quad1 (1 + 1) = correction_D_quad1 1 + correction_D_quad1 1 := hadd 1 1
212 unfold correction_D_quad1 at h11
213 norm_num at h11
214
215/-- D²/6 is not axis-additive (witness: 1+1). -/
216theorem D_quad2_not_axisAdditive : ¬ AxisAdditive correction_D_quad2 := by
217 intro h
218 rcases h with ⟨h0, hadd⟩
219 have h11 : correction_D_quad2 (1 + 1) = correction_D_quad2 1 + correction_D_quad2 1 := hadd 1 1
220 unfold correction_D_quad2 at h11
221 norm_num at h11
222
223/-! ## Part 7: Main statement (uniqueness within the admissible class) -/
224
225/-- **Main theorem**: any admissible correction is exactly `D/2`. -/
226theorem tau_correction_unique_admissible (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
227 ∀ d : ℕ, f d = correction_D_half d := by