The quadratic force in shifted, scaled form

Proved

QuadraticWell.force_shift

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

golden-rationondimensionalizationordinary-differential-equations

Let $r_1 \neq r_2$ be real, $m = (r_1 + r_2)/2$ , and $d = (r_1 - r_2)/2$ or $d = (r_2 - r_1)/2$ . Then for all real $a$ and $y$ ,

-a\,(y - r_1)(y - r_2) = -a\,d^2\left(\left(\frac{y - m}{d}\right)^2 - 1\right).

Preamble

import Mathlib

Formal statement

namespace QuadraticWell

theorem force_shift (a r₁ r₂ d : ℝ) (hr : r₁ ≠ r₂)
    (hd : d = (r₁ - r₂) / 2 ∨ d = (r₂ - r₁) / 2) (y : ℝ) :
    -a * (y - r₁) * (y - r₂) = -a * d ^ 2 * (((y - (r₁ + r₂) / 2) / 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.force_shift. Let $a, r_1, r_2, d \in \mathbb{R}$ be arbitrary real numbers, and assume:

$r_1 \neq r_2$ ;
$d$ is half the gap between $r_1$ and $r_2$ , with either sign:

d = \frac{r_1 - r_2}{2} \quad\text{or}\quad d = \frac{r_2 - r_1}{2}.

Then for every real number $y$ the following equality of real numbers holds:

-a\,(y - r_1)(y - r_2) \;=\; -a\, d^2 \left( \left( \frac{y - \frac{r_1 + r_2}{2}}{d} \right)^{2} - 1 \right).

Remarks on scope and edge cases:

No condition is placed on $a$ : it may be positive, negative, or zero (when $a = 0$ both sides are $0$ ).
No condition is placed on $y$ ; the equality is asserted for every real $y$ , including $y = r_1$ , $y = r_2$ , and the midpoint $y = \frac{r_1+r_2}{2}$ .
The division by $d$ is real division as in Mathlib, where dividing by $0$ gives $0$ . Under the stated hypotheses $d \neq 0$ , since $r_1 \neq r_2$ forces $\frac{r_1 - r_2}{2} \neq 0$ and $\frac{r_2 - r_1}{2} \neq 0$ . So the division-by-zero convention is never used, and the hypotheses on $r_1, r_2, d$ can be satisfied (for example $r_1 = 0$ , $r_2 = 2$ , $d = -1$ or $d = 1$ ).
The divisions by $2$ are ordinary real division.
The statement is a single universally quantified identity: it holds for all $a, r_1, r_2, d, y$ meeting the two hypotheses above. It makes no claim about anything physical such as forces or wells; "QuadraticWell" is only the namespace name, and no project-specific definitions appear in the statement.

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