gapAffineLogR

formal source

  36noncomputable section
  37
  38/-- Affine-log candidate family on reals. -/
  39def gapAffineLogR (a b c x : ℝ) : ℝ :=
  40  a * Real.log (1 + x / b) + c
  41
  42/-- Integer specialization. -/
  43def gapAffineLog (a b c : ℝ) (Z : ℤ) : ℝ :=
  44  gapAffineLogR a b c (Z : ℝ)
  45
  46/-- `φ = 1 + 1/φ` (golden ratio identity). -/
  47lemma phi_eq_one_add_inv_phi : phi = 1 + (1 : ℝ) / phi := by
  48  have hne : phi ≠ 0 := phi_ne_zero
  49  calc
  50    phi = phi ^ 2 / phi := by field_simp [hne]
  51    _ = (phi + 1) / phi := by simp [phi_sq_eq]
  52    _ = 1 + (1 : ℝ) / phi := by field_simp [hne]
  53
  54lemma one_add_inv_phi_eq_phi : 1 + (1 : ℝ) / phi = phi :=
  55  phi_eq_one_add_inv_phi.symm
  56
  57lemma log_one_add_inv_phi_eq_log_phi : Real.log (1 + phi⁻¹) = Real.log phi := by
  58  have hshift : (1 + phi⁻¹ : ℝ) = phi := by
  59    simpa [one_div] using one_add_inv_phi_eq_phi
  60  simp [hshift]
  61
  62/-! ## Step 1: g(0) = 0 forces c = 0 -/
  63
  64lemma zero_normalization_forces_offset
  65    {a c : ℝ}
  66    (h0 : gapAffineLogR a phi c 0 = 0) :
  67    c = 0 := by
  68  simpa [gapAffineLogR] using h0
  69