 226  rw [affine_log_collapses_to_canonical_gap h0₂ h1₂ Z]
 227
 228/-- Compact certificate for the three-point affine-log forcing closure. -/
 229structure ThreePointAffineLogClosure (a b c : ℝ) where
 230  shift_forced : b = phi
 231  scale_forced : a = 1 / Real.log phi
 232  offset_forced : c = 0
 233  collapses_to_gap : ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z
 234
 235/-- Build the closure certificate from three-point calibration data. -/
 236theorem three_point_affine_log_closure
 237    {a b c : ℝ}
 238    (hb : 1 < b)
 239    (h0 : gapAffineLogR a b c 0 = 0)
 240    (h1 : gapAffineLogR a b c 1 = 1)
 241    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 242    ThreePointAffineLogClosure (a := a) (b := b) (c := c) := by
 243  have hparams : b = phi ∧ a = 1 / Real.log phi ∧ c = 0 :=
 244    affine_log_parameters_forced_by_three_point_calibration hb h0 h1 hneg1
 245  refine ⟨hparams.1, hparams.2.1, hparams.2.2, ?_⟩
 246  exact affine_log_collapses_from_three_point_calibration hb h0 h1 hneg1
 247
 248end
 249end GapFunctionForcing
 250end Masses
 251end IndisputableMonolith

papers checked against this theorem

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