IndisputableMonolith.Masses.GapFunctionForcing

   1import Mathlib
   2import IndisputableMonolith.Constants
   3import IndisputableMonolith.Masses.RSBridge.Anchor
   4
   5/-!
   6# Gap Function Forcing (Constrained Family Closure)
   7
   8This module records a concrete closure step for Tier 1.1:
   9within a natural affine-log candidate family,
  10
  11  `g(x) = a * log(1 + x / b) + c`,
  12
  13the current closures are:
  14
  151. with fixed `b = φ`, the normalizations `g(0)=0` and `g(1)=1` force
  16   the canonical coefficients;
  172. adding a backward-step calibration `g(-1) = -2` with `b > 1` forces
  18   the shift itself: `b = φ`.
  19
  20Together, this removes all free affine-log parameters under the
  21three-point normalization and collapses the family to
  22
  23  `gap(Z) = log(1 + Z/φ) / log(φ)`.
  24
  25This does not yet prove that the affine-log family itself is uniquely forced
  26from T0–T8, but it removes coefficient freedom once that family is adopted.
  27-/
  28
  29namespace IndisputableMonolith
  30namespace Masses
  31namespace GapFunctionForcing
  32
  33open Constants
  34
  35noncomputable section
  36
  37/-- Affine-log candidate family on reals. -/
  38def gapAffineLogR (a b c x : ℝ) : ℝ :=
  39  a * Real.log (1 + x / b) + c
  40
  41/-- Integer specialization of the affine-log family. -/
  42def gapAffineLog (a b c : ℝ) (Z : ℤ) : ℝ :=
  43  gapAffineLogR a b c (Z : ℝ)
  44
  45/-- `φ = 1 + 1/φ`, used to normalize the unit-step condition. -/
  46lemma phi_eq_one_add_inv_phi : phi = 1 + (1 : ℝ) / phi := by
  47  have hphi_ne_zero : phi ≠ 0 := phi_ne_zero
  48  calc
  49    phi = phi ^ 2 / phi := by
  50      field_simp [hphi_ne_zero]
  51    _ = (phi + 1) / phi := by simp [phi_sq_eq]
  52    _ = 1 + (1 : ℝ) / phi := by
  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
  87  exact (eq_div_iff hlog_ne).2 hmul
  88
  89/-- Three-point calibration (`x = -1,0,1`) forces the affine-log shift to `b = φ`.
  90    The extra `b > 1` assumption encodes the physically relevant positive-shift branch. -/
  91lemma minus_one_step_forces_phi_shift
  92    {a b c : ℝ}
  93    (hb : 1 < b)
  94    (h0 : gapAffineLogR a b c 0 = 0)
  95    (h1 : gapAffineLogR a b c 1 = 1)
  96    (hneg1 : gapAffineLogR a b c (-1) = -2) :
  97    b = phi := by
  98  have hb_pos : 0 < b := lt_trans zero_lt_one hb
  99  have hb_ne : b ≠ 0 := ne_of_gt hb_pos
 100  have hplus_pos : 0 < 1 + (1 : ℝ) / b := by
 101    have hinv_pos : 0 < (1 : ℝ) / b := one_div_pos.mpr hb_pos
 102    linarith
 103  have hinv_lt_one : (1 : ℝ) / b < 1 := by
 104    simpa using (one_div_lt_one_div_of_lt (by norm_num : (0 : ℝ) < 1) hb)
 105  have hminus_pos : 0 < 1 - (1 : ℝ) / b := by
 106    linarith
 107  have hminus_ne : (1 - (1 : ℝ) / b) ≠ 0 := ne_of_gt hminus_pos
 108  have hc : c = 0 := by
 109    simpa [gapAffineLogR] using h0
 110  have h1' : a * Real.log (1 + (1 : ℝ) / b) = 1 := by
 111    simpa [gapAffineLogR, hc] using h1
 112  have hneg1_raw : a * Real.log (1 + (-1 : ℝ) / b) = -2 := by
 113    simpa [gapAffineLogR, hc] using hneg1
 114  have hneg1' : a * Real.log (1 - (1 : ℝ) / b) = -2 := by
 115    simpa [sub_eq_add_neg, div_eq_mul_inv, mul_assoc] using hneg1_raw
 116  have ha_ne : a ≠ 0 := by
 117    intro ha
 118    have h1'' := h1'
 119    simp [ha] at h1''
 120  have hscaled : a * (-2 * Real.log (1 + (1 : ℝ) / b)) = -2 := by
 121    calc
 122      a * (-2 * Real.log (1 + (1 : ℝ) / b))
 123          = (-2) * (a * Real.log (1 + (1 : ℝ) / b)) := by ring
 124      _ = (-2) * 1 := by rw [h1']
 125      _ = -2 := by ring
 126  have hlog_rel :
 127      Real.log (1 - (1 : ℝ) / b) = -2 * Real.log (1 + (1 : ℝ) / b) := by
 128    apply (mul_left_cancel₀ ha_ne)
 129    calc
 130      a * Real.log (1 - (1 : ℝ) / b) = -2 := hneg1'
 131      _ = a * (-2 * Real.log (1 + (1 : ℝ) / b)) := by
 132        symm
 133        exact hscaled
 134  have hlog_pow :
 135      Real.log ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) =
 136        2 * Real.log (1 + (1 : ℝ) / b) := by
 137    exact Real.log_rpow hplus_pos (2 : ℝ)
 138  have hlog_sum :
 139      Real.log (1 - (1 : ℝ) / b) +
 140        Real.log ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) = 0 := by
 141    linarith [hlog_rel, hlog_pow]
 142  have hpow_ne : ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) ≠ 0 := by
 143    exact ne_of_gt (Real.rpow_pos_of_pos hplus_pos (2 : ℝ))
 144  have hlog_prod :
 145      Real.log ((1 - (1 : ℝ) / b) * ((1 + (1 : ℝ) / b) ^ (2 : ℝ))) = 0 := by
 146    calc
 147      Real.log ((1 - (1 : ℝ) / b) * ((1 + (1 : ℝ) / b) ^ (2 : ℝ)))
 148          = Real.log (1 - (1 : ℝ) / b) + Real.log ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) := by
 149              simpa using (Real.log_mul hminus_ne hpow_ne)
 150      _ = 0 := hlog_sum
 151  have hprod_pos : 0 < (1 - (1 : ℝ) / b) * ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) := by
 152    exact mul_pos hminus_pos (Real.rpow_pos_of_pos hplus_pos (2 : ℝ))
 153  have hprod_eq_one : (1 - (1 : ℝ) / b) * ((1 + (1 : ℝ) / b) ^ (2 : ℝ)) = 1 := by
 154    exact Real.eq_one_of_pos_of_log_eq_zero hprod_pos hlog_prod
 155  have hpoly : b ^ 2 - b - 1 = 0 := by
 156    have htmp : (1 - (1 : ℝ) / b) * (1 + (1 : ℝ) / b) ^ 2 = 1 := by
 157      simpa [Real.rpow_two] using hprod_eq_one
 158    field_simp [hb_ne] at htmp
 159    nlinarith [htmp]
 160  have hphi_poly : phi ^ 2 - phi - 1 = 0 := by
 161    linarith [phi_sq_eq]
 162  have hfactor : (b - phi) * (b + phi - 1) = 0 := by
 163    nlinarith [hpoly, hphi_poly]
 164  rcases mul_eq_zero.mp hfactor with hroot | hother
 165  · linarith
 166  · have hpos : 0 < b + phi - 1 := by
 167      linarith [hb, one_lt_phi]
 168    exact False.elim ((ne_of_gt hpos) hother)
 169
 170/-- Under the three-point calibration, all affine-log parameters are forced. -/
 171theorem affine_log_parameters_forced_by_three_point_calibration
 172    {a b c : ℝ}
 173    (hb : 1 < b)
 174    (h0 : gapAffineLogR a b c 0 = 0)
 175    (h1 : gapAffineLogR a b c 1 = 1)
 176    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 177    b = phi ∧ a = 1 / Real.log phi ∧ c = 0 := by
 178  have hbphi : b = phi := minus_one_step_forces_phi_shift hb h0 h1 hneg1
 179  have h0phi : gapAffineLogR a phi c 0 = 0 := by simpa [hbphi] using h0
 180  have h1phi : gapAffineLogR a phi c 1 = 1 := by simpa [hbphi] using h1
 181  have ha : a = 1 / Real.log phi := unit_step_forces_log_scale h0phi h1phi
 182  have hc : c = 0 := zero_normalization_forces_offset h0phi
 183  exact ⟨hbphi, ha, hc⟩
 184
 185/-- Under the structural normalizations, the affine-log family is exactly the canonical gap. -/
 186theorem affine_log_collapses_to_canonical_gap
 187    {a c : ℝ}
 188    (h0 : gapAffineLogR a phi c 0 = 0)
 189    (h1 : gapAffineLogR a phi c 1 = 1) :
 190    ∀ Z : ℤ, gapAffineLog a phi c Z = RSBridge.gap Z := by
 191  have hc : c = 0 := zero_normalization_forces_offset h0
 192  have ha : a = 1 / Real.log phi := unit_step_forces_log_scale h0 h1
 193  intro Z
 194  unfold gapAffineLog gapAffineLogR RSBridge.gap
 195  calc
 196    a * Real.log (1 + (Z : ℝ) / phi) + c
 197        = (1 / Real.log phi) * Real.log (1 + (Z : ℝ) / phi) := by
 198            simp [ha, hc]
 199    _ = Real.log (1 + (Z : ℝ) / phi) / Real.log phi := by
 200          simp [div_eq_mul_inv, mul_comm]
 201
 202/-- Three-point calibration gives direct collapse to the canonical RS gap on `ℤ`. -/
 203theorem affine_log_collapses_from_three_point_calibration
 204    {a b c : ℝ}
 205    (hb : 1 < b)
 206    (h0 : gapAffineLogR a b c 0 = 0)
 207    (h1 : gapAffineLogR a b c 1 = 1)
 208    (hneg1 : gapAffineLogR a b c (-1) = -2) :
 209    ∀ Z : ℤ, gapAffineLog a b c Z = RSBridge.gap Z := by
 210  have hbphi : b = phi := minus_one_step_forces_phi_shift hb h0 h1 hneg1
 211  have h0phi : gapAffineLogR a phi c 0 = 0 := by simpa [hbphi] using h0
 212  have h1phi : gapAffineLogR a phi c 1 = 1 := by simpa [hbphi] using h1
 213  intro Z
 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
 248end
 249end GapFunctionForcing
 250end Masses
 251end IndisputableMonolith
 252