LemmaStatement: AI-adaptedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-26

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.

A reduced positive-definite form of discriminant $Δ$ satisfies $a \leq \sqrt{∣ Δ ∣ / 3}$

Statement

Let $(a, b, c)$ be a reduced positive-definite binary quadratic form with discriminant $Δ$ . Then

$a \leq \sqrt{∣ Δ ∣ / 3} .$

Facts & Assumptions

Given: A reduced positive-definite form $(a, b, c)$ with discriminant $Δ$ .

[F1]

Reduced forms satisfy $∣ b ∣ \leq a \leq c$ (Reduced positive-definite binary quadratic forms).

[F2]

The discriminant of $(a, b, c)$ is $Δ = b^{2} - 4 a c$ (The discriminant of a binary quadratic form).

[L1]

Positive-definite forms have negative discriminant (An integral binary quadratic form is positive definite exactly when its leading coefficient is positive and its discriminant is negative).

Proof

technique · direct

1.1

From $∣ b ∣ \leq a \leq c$ we get $b^{2} \leq a^{2} \leq a c$ .

F1algebra

2.1

Since the form is positive definite, [L1] gives $Δ < 0$ , so $∣ Δ ∣ = 4 a c - b^{2}$ . Using step 1.1 yields $∣ Δ ∣ = 4 a c - b^{2} \geq 4 a^{2} - a^{2} = 3 a^{2}$ .

F2L1step 1.1algebra

3.1

Therefore $a^{2} \leq ∣ Δ ∣ / 3$ , and since $a > 0$ for a positive-definite form, taking square roots gives $a \leq \sqrt{∣ Δ ∣ / 3}$ .

F1step 2.1algebra∎

Depends on

Used by

Dependency tree · two levels

5 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

William Stein, Elementary Number Theory and Elliptic Curves, proof of Proposition 9.4.1 (standard reference, not scraped)

A reduced positive-definite form of discriminant ΔΔ satisfies a≤∣Δ∣/3a≤∣Δ∣/3​