anomalous_nu_correction_zero

formal source

 138    matching the denominator. -/
 139def anomalous_nu_correction (D η : ℝ) : ℝ := η / (D + η)
 140
 141theorem anomalous_nu_correction_zero (D : ℝ) :
 142    anomalous_nu_correction D 0 = 0 := by
 143  unfold anomalous_nu_correction; simp
 144
 145/-- For small η, the anomalous correction ≈ η/D, i.e. the correction rate
 146    at leading order is 1/D per unit of η. -/
 147theorem anomalous_nu_correction_small (D η : ℝ) (hD : 0 < D) (hη : 0 ≤ η) :
 148    anomalous_nu_correction D η ≤ η / D := by
 149  unfold anomalous_nu_correction
 150  have hDη : 0 < D + η := by linarith
 151  have hDη_ne : D + η ≠ 0 := ne_of_gt hDη
 152  have hD_ne : D ≠ 0 := ne_of_gt hD
 153  rcases eq_or_lt_of_le hη with rfl | hη_pos
 154  · simp
 155  · rw [div_le_div_iff₀ hDη hD]
 156    nlinarith
 157
 158/-- The corrected ν₀ + η/(D + η). -/
 159def nu_corrected (D η : ℝ) : ℝ :=
 160  nu_leading + anomalous_nu_correction D η
 161
 162theorem nu_corrected_at_zero (D : ℝ) :
 163    nu_corrected D 0 = nu_leading := by
 164  unfold nu_corrected; rw [anomalous_nu_correction_zero]; ring
 165
 166/-- The Q₃ spectral-gap multiplicity equals the graph degree D = 3.
 167    This is the structural reason why D = 3 appears in the denominator
 168    of the anomalous correction. -/
 169theorem spectral_gap_multiplicity_eq_degree :
 170    Q3_multiplicities = [1, Q3_degree, Q3_degree, 1] := by
 171  unfold Q3_multiplicities Q3_degree; native_decide