The sign of $d$ can be chosen so that $a d > 0$

Proved

QuadraticWell.sign_choice

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

a\,\frac{r_1 - r_2}{2} > 0 \qquad\text{or}\qquad a\,\frac{r_2 - r_1}{2} > 0 ,

so for one choice of $d = \pm(r_1 - r_2)/2$ the time scale $\omega = \sqrt{a d}$ is real and positive.

Preamble

import Mathlib

Formal statement

namespace QuadraticWell

theorem sign_choice (a r₁ r₂ : ℝ) (ha : a ≠ 0) (hr : r₁ ≠ r₂) :
    0 < a * ((r₁ - r₂) / 2) ∨ 0 < a * ((r₂ - r₁) / 2) := 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.sign_choice. Let $a$ , $r_1$ and $r_2$ be arbitrary real numbers, all universally quantified. There are no other variables and no typeclass assumptions. The statement has two hypotheses:

$a \neq 0$ ;
$r_1 \neq r_2$ .

Under these hypotheses, the statement asserts that at least one of two strict inequalities holds (an inclusive "or"):

0 < a \cdot \frac{r_1 - r_2}{2} \qquad\text{or}\qquad 0 < a \cdot \frac{r_2 - r_1}{2}.

Here $\frac{\cdot}{2}$ is ordinary real division by the nonzero constant $2$ . No division by zero or other junk value occurs. The statement does not say which of the two disjuncts holds, and it does not claim that exactly one holds. Both hypotheses can be satisfied (for example $a = 1$ , $r_1 = 1$ , $r_2 = 0$ ), so the statement is not vacuous. The cases $a = 0$ and $r_1 = r_2$ are excluded by the hypotheses, and the statement says nothing about them. In both of those cases each product is $0$ , so neither strict inequality would hold. No other relationship between $a$ , $r_1$ and $r_2$ is assumed: $a$ may be positive or negative, and $r_1$ may be larger or smaller than $r_2$ .

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

The sign of ddd can be chosen so that ad>0a d > 0ad>0

The sign of $d$ can be chosen so that $a d > 0$