affine_log_unique_under_normalizations

formal source

 214  simpa [hbphi] using affine_log_collapses_to_canonical_gap h0phi h1phi Z
 215
 216/-- Uniqueness in the constrained affine-log class. -/
 217theorem affine_log_unique_under_normalizations
 218    {a₁ c₁ a₂ c₂ : ℝ}
 219    (h0₁ : gapAffineLogR a₁ phi c₁ 0 = 0)
 220    (h1₁ : gapAffineLogR a₁ phi c₁ 1 = 1)
 221    (h0₂ : gapAffineLogR a₂ phi c₂ 0 = 0)
 222    (h1₂ : gapAffineLogR a₂ phi c₂ 1 = 1) :
 223    ∀ Z : ℤ, gapAffineLog a₁ phi c₁ Z = gapAffineLog a₂ phi c₂ Z := by
 224  intro Z
 225  rw [affine_log_collapses_to_canonical_gap h0₁ h1₁ Z]
 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