deriv_pos_self_zero
plain-language theorem explainer
If a differentiable real-valued function satisfies the ODE h' = h together with the initial condition h(0) = 0, then h vanishes identically. Workers proving uniqueness of the J-cost functional at the T5 step of the Recognition Science chain cite this auxiliary result. The argument multiplies h by the damping factor exp(-t), shows the product has vanishing derivative, and recovers the zero function from the constant value fixed at t = 0.
Claim. Let $h : ℝ → ℝ$ be differentiable. If $h'(t) = h(t)$ for every real $t$ and $h(0) = 0$, then $h(t) = 0$ for every real $t$.
background
The lemma sits inside the Functional Equation Helpers for T5 module, whose purpose is to supply calculus identities needed for the uniqueness proof of the J-cost. The J-cost is the function obeying the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y) and is realized concretely by cosh(log x) - 1. The argument imports the helper deriv_exp_neg, which states that the derivative of exp(-s) equals -exp(-s), together with the standard Mathlib fact is_const_of_deriv_eq_zero.
proof idea
Form the auxiliary map s ↦ h(s)·exp(-s). Its derivative expands by the product rule to h'(s)exp(-s) + h(s)·(-exp(-s)). Substitute the given relation h' = h and the identity deriv_exp_neg to obtain zero. Differentiability of the product follows from the product of differentiable maps. Apply is_const_of_deriv_eq_zero to conclude the auxiliary map is constant. The constant equals h(0)·exp(0) = 0. Division by the strictly positive factor exp(-t) then yields h(t) = 0.
why it matters
The lemma is invoked directly by ode_zero_uniqueness, the theorem that asserts the only C² solution of f'' = f with f(0) = f'(0) = 0 is the zero function. That uniqueness statement closes the T5 J-uniqueness step in the forcing chain, confirming that the only automorphism satisfying the Recognition Composition Law is the hyperbolic-cosine form. The result therefore supports the subsequent derivation of the self-similar fixed point phi and the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.