axisAdditive_linear

formal source

 124  f 0 = 0 ∧ ∀ a b : ℕ, f (a + b) = f a + f b
 125
 126/-- Any axis-additive function on ℕ is linear: f(d) = d * f(1). -/
 127theorem axisAdditive_linear (f : ℕ → ℝ) (h : AxisAdditive f) :
 128    ∀ d : ℕ, f d = (d : ℝ) * f 1 := by
 129  rcases h with ⟨h0, hadd⟩
 130  intro d
 131  induction d with
 132  | zero =>
 133      simp [h0]
 134  | succ d ih =>
 135      -- f(d+1) = f(d) + f(1)
 136      have hstep : f (d + 1) = f d + f 1 := by
 137        simpa using (hadd d 1)
 138      -- expand and use IH
 139      calc
 140        f (Nat.succ d) = f d + f 1 := by
 141          simpa [Nat.succ_eq_add_one] using hstep
 142        _ = ((d : ℝ) * f 1) + f 1 := by simpa [ih]
 143        _ = ((d : ℝ) + 1) * f 1 := by ring
 144        _ = ((Nat.succ d : ℝ) * f 1) := by
 145          simp [Nat.cast_succ, add_comm, add_left_comm, add_assoc]
 146
 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