one_add_inv_phi_eq_phi

formal source

  53      field_simp [hphi_ne_zero]
  54
  55/-- Equivalent rewrite of `1 + 1/φ = φ`. -/
  56lemma one_add_inv_phi_eq_phi : 1 + (1 : ℝ) / phi = phi := by
  57  simpa using phi_eq_one_add_inv_phi.symm
  58
  59/-- Log rewrite at the canonical shift argument. -/
  60lemma log_one_add_inv_phi_eq_log_phi : Real.log (1 + phi⁻¹) = Real.log phi := by
  61  have hshift : (1 + phi⁻¹ : ℝ) = phi := by
  62    simpa [one_div] using one_add_inv_phi_eq_phi
  63  simp [hshift]
  64
  65/-- Neutral normalization fixes the additive offset. -/
  66lemma zero_normalization_forces_offset
  67    {a c : ℝ}
  68    (h0 : gapAffineLogR a phi c 0 = 0) :
  69    c = 0 := by
  70  simpa [gapAffineLogR] using h0
  71
  72/-- Unit-step calibration fixes the log scale coefficient. -/
  73lemma unit_step_forces_log_scale
  74    {a c : ℝ}
  75    (h0 : gapAffineLogR a phi c 0 = 0)
  76    (h1 : gapAffineLogR a phi c 1 = 1) :
  77    a = 1 / Real.log phi := by
  78  have hc : c = 0 := zero_normalization_forces_offset h0
  79  have hlog_ne : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)
  80  have hmul_raw : a * Real.log (1 + phi⁻¹) = 1 := by
  81    simpa [gapAffineLogR, hc] using h1
  82  have hmul : a * Real.log phi = 1 := by
  83    calc
  84      a * Real.log phi = a * Real.log (1 + phi⁻¹) := by
  85        rw [log_one_add_inv_phi_eq_log_phi]
  86      _ = 1 := hmul_raw