alphaInv_linear_term

formal source

 197
 198/-- The first-order (linear) term of α⁻¹ in f_gap: matches a naive
 199    perturbative expansion. -/
 200theorem alphaInv_linear_term :
 201    alphaInv_of_gap 0 = alpha_seed := by
 202  unfold alphaInv_of_gap
 203  simp [Real.exp_zero]
 204
 205/-- The first derivative at f_gap = 0: rate of decrease is -1 per unit
 206    gap (independent of α_seed at leading order). -/
 207theorem alphaInv_linear_rate :
 208    deriv alphaInv_of_gap 0 = -1 := by
 209  rw [deriv_alphaInv_of_gap]
 210  rw [alphaInv_linear_term]
 211  field_simp
 212
 213/-! ## Part 5: The Uniqueness Question (Open)
 214
 215A full forcing argument would prove that the exponential form is the
 216UNIQUE form satisfying certain structural constraints. The simplest
 217candidate uniqueness statement:
 218
 219Given a function g : ℝ → ℝ such that:
 2201. g is smooth (C^∞)
 2212. g(0) = α_seed and g'(0) = -1 (so leading-order behavior matches
 222   α_seed - f_gap)
 2233. The logarithmic derivative (log g)'(x) is CONSTANT (equal to -1/α_seed)
 224
 225Then g(x) = α_seed · exp(-x/α_seed).
 226
 227Condition (3) is the distinctive feature: it says the relative rate of
 228change of g is scale-free (same at all x). This IS a forcing property
 229(standard ODE uniqueness), but it is also a STRUCTURAL ASSUMPTION that
 230needs physical justification in the RS context.