Corollary: the golden-ratio well is the normal form in disguise

Proved

QuadraticWell.golden_well

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

golden-rationondimensionalizationordinary-differential-equations

For every twice continuously differentiable $x : \mathbb{R} \to \mathbb{R}$ ,

\bigl(\forall t,\ x''(t) = -(x(t)^2 - x(t) - 1)\bigr) \iff \bigl(\forall \tau,\ z''(\tau) = -(z(\tau)^2 - 1)\bigr), \qquad z(\tau) = \frac{x(\tau/\omega) - \tfrac12}{\sqrt5/2},\quad \omega = \sqrt{\sqrt5/2}.

The well $x^2 - x - 1$ has roots $\varphi$ and $-1/\varphi$ ; its $\varphi$ is a choice of coordinates.

Preamble

import Mathlib

Formal statement

namespace QuadraticWell

theorem golden_well (x : ℝ → ℝ) (hx : ContDiff ℝ 2 x) :
    (∀ t, deriv (deriv x) t = -(x t ^ 2 - x t - 1)) ↔
    (∀ τ, deriv (deriv (fun σ => (x (σ / Real.sqrt (Real.sqrt 5 / 2)) - 1 / 2) /
        (Real.sqrt 5 / 2))) τ =
      -(((x (τ / Real.sqrt (Real.sqrt 5 / 2)) - 1 / 2) / (Real.sqrt 5 / 2)) ^ 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.golden_well. Let $x:\mathbb{R}\to\mathbb{R}$ be any real function that is $C^2$ on all of $\mathbb{R}$ , meaning twice differentiable everywhere with continuous second derivative. This is the only hypothesis, and there are no other parameters. Write $x''$ for the ordinary second derivative of $x$ . The code computes it as the derivative of the derivative. Because $x$ is $C^2$ , this equals the classical second derivative at every point, so Mathlib's convention that a non-differentiable function has "derivative $0$ " never comes into play. Fix the two positive constants

c=\frac{\sqrt5}{2}\approx 1.118,\qquad s=\sqrt{c}=\sqrt{\tfrac{\sqrt5}{2}}\approx 1.057 .

Both square roots are taken of positive numbers, so no junk values from $\sqrt{\cdot}$ or division arise. Define the rescaled and shifted function

y(\sigma)=\frac{x(\sigma/s)-\tfrac12}{c}\qquad(\sigma\in\mathbb{R}).

$y$ is also $C^2$ on $\mathbb{R}$ , so its iterated derivative $y''$ is its classical second derivative.

The theorem asserts a two-sided equivalence (an "if and only if") between the following two statements.

For every real $t$ ,

x''(t) = -\bigl(x(t)^2 - x(t) - 1\bigr).

For every real $\tau$ ,

y''(\tau) = -\bigl(y(\tau)^2 - 1\bigr) = 1 - y(\tau)^2 .

Written out in terms of $x$ , the left side is the second derivative at $\tau$ of $\sigma\mapsto \bigl(x(\sigma/\sqrt{\sqrt5/2})-\tfrac12\bigr)\big/(\sqrt5/2)$ . The right side is $-\Bigl(\bigl(\tfrac{x(\tau/\sqrt{\sqrt5/2})-1/2}{\sqrt5/2}\bigr)^2-1\Bigr)$ .

In words: a $C^2$ function $x$ satisfies the ODE $x''=-(x^2-x-1)$ at every point of $\mathbb{R}$ exactly when the function $y$ , obtained by time-rescaling with $\sigma = s\,t$ and the affine change $y = (x-\tfrac12)/c$ , satisfies $y''=1-y^2$ at every point of $\mathbb{R}$ . Both ODE conditions are global, holding for all real times. Neither is restricted to an interval, and no initial conditions are imposed. The statement makes no claim about existence or uniqueness of solutions, or about any particular solution. It only asserts that the two pointwise-everywhere conditions are equivalent for every $C^2$ function $x$ .

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