LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (openai/gpt-5.4)audited 2026-07-25

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced — the exact statement appears in a cited source; only wording and notation differ.
AI-adapted — a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated — a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Squaring is monotone on the nonnegatives

Statement

Let $F$ be an ordered field. For $a, b \ge 0$ :

$a < b \iff a^2 < b^2, \qquad a \le b \iff a^2 \le b^2.$

More generally, for arbitrary $a, b \in F$ , $a^2 < b^2 \iff |a| < |b|$ .

Facts & Assumptions

Given: Elements $a, b$ of an ordered field $F$ .

[L1]

For a positive factor $s > 0$ and any $t$ : $t > 0 \iff st > 0$ ; this is Sign rules for products and monotonicity of multiplication (the rule $c > 0 \Rightarrow (x < y \iff xc < yc)$ taken at $x = 0$ , $y = t$ , $c = s$ , using $0 \cdot s = 0$ , Multiplication by zero: $0 \cdot a = 0$ ).

[L2]

Trichotomy: for $a, b$ exactly one of $a < b$ , $a = b$ , $a > b$ holds; and a sum of two nonnegatives with at least one positive is positive (Ordered field).

[L3]

$|x| \ge 0$ and $|x|^2 = x^2$ for every $x$ (Basic properties of the absolute value).

Proof

technique · direct

1.1

The difference factors as $b^2 - a^2 = (b - a)(b + a)$ .

algebra

2.1

If $a, b \ge 0$ and $a < b$ , then $b > 0$ , so $b + a > 0$ by [L2], and $b - a > 0$ ; by [L1] with $s = b + a$ and $t = b - a$ , $(b - a)(b + a) > 0$ , i.e. $a^2 < b^2$ .

L1L2step 1.1

2.2

If $a, b \ge 0$ and $a^2 < b^2$ , then $b^2 - a^2 > 0$ , so $a, b$ are not both zero and $b + a > 0$ by [L2]; by [L1] with $s = b + a$ , from $(b - a)(b + a) = b^2 - a^2 > 0$ we get $b - a > 0$ , i.e. $a < b$ .

L1L2step 1.1

3.1

Hence for $a, b \ge 0$ , $a < b \iff a^2 < b^2$ .

step 2.1step 2.2

4.1

The $\le$ form follows by trichotomy: for $a, b \ge 0$ , applying step 3.1 to the nonnegatives $b, a$ gives $a \le b \iff \lnot(b < a) \iff \lnot(b^2 < a^2) \iff a^2 \le b^2$ .

step 3.1L2

5.1

For arbitrary $a, b$ , [L3] gives $|a|, |b| \ge 0$ with $|a|^2 = a^2$ and $|b|^2 = b^2$ ; applying step 3.1 to $|a|, |b|$ yields $a^2 < b^2 \iff |a|^2 < |b|^2 \iff |a| < |b|$ .

step 3.1L3∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 7 results over 5 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

W. Rudin, Principles of Mathematical Analysis, 3rd ed., Ch. 1 (standard reference, not scraped)
M. Spivak, Calculus, 4th ed., Ch. 1 (standard reference, not scraped)