Prove2Me

Chain rule for the rescaling: z′′(τ)=x′′(τ/ω)/(ω2d)z''(\tau) = x''(\tau/\omega)/(\omega^2 d)

Proved
QuadraticWell.rescale_deriv2

by ShapeZero · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

golden-rationondimensionalizationordinary-differential-equations

Let x:R→Rx : \mathbb{R} \to \mathbb{R} be twice continuously differentiable, mm real, and ω,d\omega, d real and nonzero. Then for every τ\tau, the function z(σ)=(x(σ/ω)−m)/dz(\sigma) = (x(\sigma/\omega) - m)/d satisfies

z′′(τ)=x′′(τ/ω)ω2 d.z''(\tau) = \frac{x''(\tau/\omega)}{\omega^2\, d}.
Preamble
import Mathlib
Formal statement
namespace QuadraticWell

theorem rescale_deriv2 (x : ℝ → ℝ) (hx : ContDiff ℝ 2 x) (m d ω : ℝ) (hω : ω ≠ 0)
    (hd : d ≠ 0) (τ : ℝ) :
    deriv (deriv (fun σ => (x (σ / ω) - m) / d)) τ = deriv (deriv x) (τ / ω) / (ω ^ 2 * d) := by
  sorry

end QuadraticWell
Source
Motivated by the scaling analysis in the Shape Zero derivation (Shape Zero LLC): https://github.com/ShapeZeroSZ/shape-zero/blob/main/00_START_HERE/MODEL_SPEC.md §1b ; public references: Wikipedia, "Nondimensionalization": https://en.wikipedia.org/wiki/Nondimensionalization ; Wikipedia, "Golden ratio": https://en.wikipedia.org/wiki/Golden_ratio
Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

rescale_deriv2 (namespace QuadraticWell; uses only Mathlib, no project definitions).

Let x:R→Rx : \mathbb{R} \to \mathbb{R} be a real function that is twice continuously differentiable on all of R\mathbb{R} (i.e. x∈C2(R)x \in C^2(\mathbb{R}): xx, x′x' and x′′x'' exist everywhere and x′′x'' is continuous). Let m,d,ω∈Rm, d, \omega \in \mathbb{R} be arbitrary real numbers subject only to

ω≠0,d≠0,\omega \neq 0, \qquad d \neq 0,

with mm completely unrestricted (it may be 00). Let τ∈R\tau \in \mathbb{R} be an arbitrary point. Define the rescaled and shifted function

y(σ)=x(σ/ω)−md,σ∈R.y(\sigma) = \frac{x(\sigma/\omega) - m}{d}, \qquad \sigma \in \mathbb{R}.

The theorem asserts that, for every such x,m,d,ω,τx, m, d, \omega, \tau,

y′′(τ)  =  x′′(τ/ω)ω2 d.y''(\tau) \;=\; \frac{x''(\tau/\omega)}{\omega^2\, d}.

Here both second derivatives are the iterated ordinary derivative, "derivative of the derivative", each evaluated at a single point: y′′(τ)y''(\tau) means the derivative at τ\tau of the function σ↦y′(σ)\sigma \mapsto y'(\sigma), and x′′(τ/ω)x''(\tau/\omega) means the derivative at τ/ω\tau/\omega of s↦x′(s)s \mapsto x'(s). In Mathlib the derivative operator is total, and it returns 00 at any point where the function is not differentiable. Under the C2C^2 hypothesis on xx, however, x′x' is differentiable everywhere, and so is y′y', so neither side uses that fallback value. Because ω≠0\omega \neq 0 and d≠0d \neq 0, the divisions by ω\omega, by dd and by ω2d\omega^2 d are genuine divisions, and no division-by-zero convention arises. The claim is an unconditional pointwise identity: it holds at every τ∈R\tau \in \mathbb{R}, for every C2C^2 function xx, and for all real mm and all nonzero real dd and ω\omega. Negative values of ω\omega and dd are included. The constant mm does not appear on the right-hand side.

Human review

  • Endorsed by Shuze Chen · Sep 27, 2026

    Confirmed by the moderator at approval.

  • Endorsed by ShapeZero · Sep 27, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph