AdmissibleCorrection

formal source

 147/-! ### Admissible correction terms -/
 148
 149/-- Admissible dimension correction: axis-additive and calibrated at D=3. -/
 150structure AdmissibleCorrection (f : ℕ → ℝ) : Prop where
 151  axisAdditive : AxisAdditive f
 152  calib_D3 : f 3 = 3 / 2
 153
 154/-- Uniqueness: any admissible correction is exactly D/2. -/
 155theorem admissible_unique (f : ℕ → ℝ) (h : AdmissibleCorrection f) :
 156    ∀ d : ℕ, f d = (d : ℝ) / 2 := by
 157  have hlin := axisAdditive_linear f h.axisAdditive
 158  -- use calibration at d=3 to solve for f(1)
 159  have h3 : f 3 = (3 : ℝ) * f 1 := hlin 3
 160  have hf1 : f 1 = (1 : ℝ) / 2 := by
 161    -- from f3 = 3/2 = 3*f1
 162    have : (3 : ℝ) * f 1 = (3 : ℝ) / 2 := by
 163      -- rewrite h3 using calib
 164      rw [← h3, h.calib_D3]
 165    -- divide by 3
 166    have h3ne : (3 : ℝ) ≠ 0 := by norm_num
 167    -- f1 = (3/2)/3 = 1/2
 168    field_simp [h3ne] at this
 169    -- `this` is now: 3 * (2 * f1) = 3  (or equivalent); solve
 170    nlinarith
 171  intro d
 172  have : f d = (d : ℝ) * f 1 := hlin d
 173  -- substitute f1 = 1/2
 174  rw [this, hf1]
 175  ring
 176
 177/-! ### Instances and exclusions -/
 178
 179/-- D/2 is admissible. -/
 180theorem D_half_admissible : AdmissibleCorrection correction_D_half := by