Every quadratic-force oscillator is $z'' = -(z^2 - 1)$ in different units

Proved

QuadraticWell.quadratic_well_equiv

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

golden-rationondimensionalizationordinary-differential-equations

Let $a \neq 0$ and $r_1 \neq r_2$ be real. Then there are real numbers $m$ , $d$ , $\omega$ with $d \neq 0$ and $\omega > 0$ , chosen once, before any solution is considered, such that for every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ :

\bigl(\forall t,\ x''(t) = -a\,(x(t) - r_1)(x(t) - r_2)\bigr) \iff \bigl(\forall \tau,\ z''(\tau) = -(z(\tau)^2 - 1)\bigr),

where $z(\tau) = (x(\tau/\omega) - m)/d$ . (Explicitly $m = (r_1 + r_2)/2$ , $d = \pm(r_1 - r_2)/2$ with $a d > 0$ , and $\omega = \sqrt{a d}$ .)

Preamble

import Mathlib

Formal statement

namespace QuadraticWell

/-- MISSION GOAL: every quadratic-force oscillator with two distinct real roots is
the normal-form oscillator z'' = -(z² - 1) after one fixed affine change of value
and one fixed rescaling of time. -/
theorem quadratic_well_equiv (a r₁ r₂ : ℝ) (ha : a ≠ 0) (hr : r₁ ≠ r₂) :
    ∃ m d ω : ℝ, d ≠ 0 ∧ 0 < ω ∧
      ∀ x : ℝ → ℝ, ContDiff ℝ 2 x →
        ((∀ t, deriv (deriv x) t = -a * (x t - r₁) * (x t - r₂)) ↔
         (∀ τ, deriv (deriv (fun σ => (x (σ / ω) - m) / d)) τ =
                -(((x (τ / ω) - m) / d) ^ 2 - 1))) := 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

QuadraticWell.quadratic_well_equiv. Let $a, r_1, r_2$ be real numbers with $a \neq 0$ and $r_1 \neq r_2$ . There are no other hypotheses. The theorem asserts that there exist real numbers $m$ , $d$ , $\omega$ with

d \neq 0 \quad\text{and}\quad \omega > 0

such that the following holds for every function $x : \mathbb{R} \to \mathbb{R}$ that is twice continuously differentiable on all of $\mathbb{R}$ ( $C^2$ ):

\Big(\forall t \in \mathbb{R}:\ x''(t) = -a\,\big(x(t) - r_1\big)\big(x(t) - r_2\big)\Big) \iff \Big(\forall \tau \in \mathbb{R}:\ y_x''(\tau) = -\big(y_x(\tau)^2 - 1\big)\Big),

where $y_x : \mathbb{R} \to \mathbb{R}$ is the rescaled function

y_x(\sigma) = \frac{x(\sigma/\omega) - m}{d}.

Here $x''$ and $y_x''$ denote the second derivative computed as the derivative of the derivative, each taken pointwise on $\mathbb{R}$ (a derivative taken where the function is not differentiable would be $0$ by convention, but since $x$ is $C^2$ and $\omega > 0$ , $d \neq 0$ , both $x$ and $y_x$ are twice differentiable everywhere, so these are the genuine second derivatives). The right-hand equation is equivalently $y_x'' = 1 - y_x^2$ .

Quantifier order. The constants $m, d, \omega$ are chosen after $a, r_1, r_2$ and may depend on them, but they are chosen before $x$ : a single triple $(m, d, \omega)$ must work uniformly for all $C^2$ functions $x$ . Nothing is asserted about uniqueness of $(m, d, \omega)$ , nor about any explicit formula for them.

Scope and edge cases.

Because $\omega > 0$ and $d \neq 0$ are guaranteed, the divisions $\sigma/\omega$ and $(\cdots)/d$ never divide by zero; no junk values arise. As $\tau$ ranges over $\mathbb{R}$ , $\tau/\omega$ also ranges over all of $\mathbb{R}$ .
Both sides of the equivalence are statements about all real times ( $t$ resp. $\tau$ ), i.e. global solutions on $\mathbb{R}$ ; nothing is said about solutions on subintervals or about initial-value problems.
The equivalence is only claimed for $C^2$ functions $x$ ; functions that are not $C^2$ are not covered.
The cases $a = 0$ or $r_1 = r_2$ are excluded by hypothesis and not addressed. The hypotheses $a \neq 0$ , $r_1 \neq r_2$ are always jointly satisfiable, so the statement is not vacuous in that sense.

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

Every quadratic-force oscillator is z′′=−(z2−1)z'' = -(z^2 - 1)z′′=−(z2−1) in different units

Every quadratic-force oscillator is $z'' = -(z^2 - 1)$ in different units