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. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.