exponential_form_from_constant_log_derivative

formal source

 239
 240/-- **Open question as a Prop**: the exponential form is uniquely
 241    determined by constant logarithmic derivative. -/
 242def exponential_form_from_constant_log_derivative : Prop :=
 243  ∀ (g : ℝ → ℝ),
 244    (g 0 = alpha_seed) →
 245    (∀ x, 0 < g x) →
 246    ContDiff ℝ ⊤ g →
 247    (∀ x, deriv (fun y => Real.log (g y)) x = -(1 / alpha_seed)) →
 248    ∀ x, g x = alpha_seed * Real.exp (-(x / alpha_seed))
 249
 250/-- **OPEN STATUS**: This uniqueness claim follows from standard ODE theory
 251    (if log g' is constant = k, then g(x) = g(0) · e^(kx), which is unique
 252    under Picard-Lindelöf). We leave it unproved here as it is provable in
 253    principle but requires ODE machinery.
 254
 255    The *physical* question — WHY the log derivative should be constant
 256    in the RS derivation — is the true remaining gap. -/
 257theorem exponential_form_uniqueness_ode_principle :
 258    True := trivial
 259
 260/-! ## Summary of What This Module Proves
 261
 2621. **Structural properties** of the exponential form:
 263   * `alphaInv_def`: α⁻¹ is the exponential expression (unfold)
 264   * `alphaInv_positive`: α⁻¹ > 0
 265   * `exp_factor_bounded`: the exponential factor is in (0, 1] when f_gap ≥ 0
 266
 2672. **Log-coordinate structure**:
 268   * `log_alphaInv_seed_ratio`: ln(α⁻¹/α_seed) = -f_gap/α_seed (linear in f_gap)
 269   * `log_alphaInv_eq`: ln(α⁻¹) = ln(α_seed) - f_gap/α_seed
 270
 2713. **Differential structure**:
 272   * `deriv_alphaInv_of_gap`: dα⁻¹/df_gap = -α⁻¹/α_seed (the defining ODE)