 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⟩
 228
 229end
 230end GapFunctionForcing
 231end RSBridge
 232end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.