three_point_forces_canonical_gap

formal source

 194          simp [div_eq_mul_inv, mul_comm]
 195
 196/-- Three-point calibration gives direct collapse to the canonical gap. -/
 197theorem three_point_forces_canonical_gap
 198    {a b c : ℝ}
 199    (hb : 1 < b)
 200    (h0 : gapAffineLogR a b c 0 = 0)
 201    (h1 : gapAffineLogR a b c 1 = 1)
 202    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 203    ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z := by
 204  have hbphi : b = phi := minus_one_step_forces_phi_shift hb h0 h1 hneg1
 205  have h0phi : gapAffineLogR a phi c 0 = 0 := by simpa [hbphi] using h0
 206  have h1phi : gapAffineLogR a phi c 1 = 1 := by simpa [hbphi] using h1
 207  intro Z
 208  simpa [hbphi] using affine_log_collapses_to_gap h0phi h1phi Z
 209
 210/-- Certificate structure for the three-point closure. -/
 211structure ThreePointClosure (a b c : ℝ) where
 212  shift_forced : b = phi
 213  scale_forced : a = 1 / Real.log phi
 214  offset_forced : c = 0
 215  collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
 216
 217/-- Build the closure certificate from calibration data. -/
 218theorem three_point_closure
 219    {a b c : ℝ}
 220    (hb : 1 < b)
 221    (h0 : gapAffineLogR a b c 0 = 0)
 222    (h1 : gapAffineLogR a b c 1 = 1)
 223    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 224    ThreePointClosure a b c := by
 225  have hparams := affine_log_parameters_forced hb h0 h1 hneg1
 226  exact ⟨hparams.1, hparams.2.1, hparams.2.2,
 227         three_point_forces_canonical_gap hb h0 h1 hneg1⟩