deriv_neg_self_zero
plain-language theorem explainer
The lemma shows that any differentiable real-valued function g satisfying g' = -g with g(0) = 0 must vanish identically. It is invoked in uniqueness arguments for linear ODEs arising in the T5 cost functional equation development. The argument forms the auxiliary product g(t) exp(t), verifies its derivative vanishes via the product rule, invokes constancy from a zero derivative, and recovers g(t) = 0 by division with the positive exponential factor.
Claim. Let $g : ℝ → ℝ$ be differentiable. If $g'(t) = -g(t)$ for all real $t$ and $g(0) = 0$, then $g(t) = 0$ for all $t$.
background
The declaration sits in the Cost.FunctionalEquation module, whose module documentation states it supplies lemmas for the T5 cost uniqueness proof. T5 establishes J-uniqueness via the functional equation J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y). The present lemma supplies a basic uniqueness fact for the auxiliary ODE g' = -g that appears when differentiating the cost functional. Upstream arithmetic definitions from ArithmeticFromLogic and IntegersFromLogic supply the underlying multiplication operations used in the broader Recognition Science development, while the local proof draws on standard real-analysis facts for the product rule and constancy under zero derivative.
proof idea
The tactic proof first establishes that the derivative of the product g(s) * exp(s) is identically zero by applying the product rule, substituting the given condition deriv g t = -g t, and simplifying. Differentiability of the product is recorded separately. The lemma is_const_of_deriv_eq_zero is then applied to conclude the product is constant. Specializing the constant at an arbitrary t and at 0, followed by algebraic rearrangement using exp(t) > 0, yields the identity g(t) = 0.
why it matters
The result is used by ode_zero_uniqueness, which states that the unique solution to f'' = f with f(0) = f'(0) = 0 is f = 0. It therefore closes a step in the T5 cost uniqueness argument inside the functional-equation module. Within the Recognition Science chain, T5 supplies J-uniqueness (J(x) = cosh(log x) - 1), which forces the self-similar fixed point phi and the eight-tick octave leading to D = 3 spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.