alphaInv_linear_rate

formal source

 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.
 231
 232Alternative formulas like α_seed / (1 + x/α_seed) have non-constant log
 233derivative ((d/dx) log(α_seed/(1+x/α_seed)) = -1/(α_seed + x), which
 234depends on x), so they don't satisfy (3).
 235
 236Whether RS structure FORCES the log-derivative to be constant is the
 237genuine open question.