deriv_exp_neg
The lemma states that the derivative of the map s to exp(-s) at any real t equals -exp(-t). Researchers proving T5 J-uniqueness in the Recognition Science cost framework cite this helper when handling exponential factors in differential equations. The proof composes the standard HasDerivAt for exp with the derivative of negation via the chain rule and simplifies.
claimFor every real number $t$, the derivative of the function $smapsto e^{-s}$ at $t$ equals $-e^{-t}$.
background
This lemma sits in the module of functional-equation helpers for the T5 cost-uniqueness argument. T5 forces the J-cost to be the unique solution of the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), with J(x) = (x + x^{-1})/2 - 1. Upstream structures include J-automorphism composition from CostAlgebra, the phi-ladder calibration in PhiForcingDerived, and the spectral emergence of gauge content in SpectralEmergence that together fix the exponential decay scale in the cost ODE.
proof idea
The tactic proof first obtains HasDerivAt for exp at -t, constructs HasDerivAt for negation at t by hasDerivAt_neg, composes them with HasDerivAt.comp, then applies simp to extract the derivative value.
why it matters in Recognition Science
The result feeds directly into deriv_pos_self_zero, which concludes that any solution h of h' = h with h(0) = 0 must vanish identically; that zero-solution step closes the uniqueness argument for the J-cost in the T5 forcing chain. It therefore anchors the exponential factors that appear when the Recognition Composition Law is differentiated.
scope and limits
- Does not prove differentiability of exp on its own.
- Does not extend the identity beyond the real line.
- Does not supply higher-order derivatives or Taylor expansions.
Lean usage
have h_const : ∀ t, deriv (fun s => h s * Real.exp (-s)) t = 0 := by rw [deriv_mul, deriv_exp_neg]formal statement (Lean)
280lemma deriv_exp_neg (t : ℝ) : deriv (fun s => Real.exp (-s)) t = -Real.exp (-t) := by
proof body
Tactic-mode proof.
281 have h := Real.hasDerivAt_exp (-t)
282 have hc : HasDerivAt (fun s => -s) (-1) t := by
283 have := hasDerivAt_neg (x := t)
284 simp at this ⊢
285 exact this
286 have hcomp := h.comp t hc
287 simp at hcomp
288 exact hcomp.deriv
289
290/-- Diagonalization of the ODE f'' = f into f' ± f components. -/