CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 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.

An indefinite proper-equivalence class can contain a cycle of reduced forms

Statement refuted

The uniqueness theorem for reduced positive-definite forms does not extend to positive discriminant. Under Granville's positive-discriminant convention, both

$f = (- 6, 6, 1) and g = (1, 6, - 6)$

are reduced forms of discriminant $60$ , and they are properly equivalent.

Facts & Assumptions

Given: The forms $f = (- 6, 6, 1)$ and $g = (1, 6, - 6)$ .

[L1]

Positive-definite proper-equivalence classes contain exactly one reduced form (Each proper-equivalence class of positive-definite integral binary quadratic forms contains exactly one reduced form).

[F1]

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

Counterexample

technique · direct

1.1

Both forms have discriminant $60$ , since $6^{2} - 4 (- 6) (1) = 60$ and $6^{2} - 4 (1) (- 6) = 60$ .

F1givenalgebra

1.2

The matrix $M = (\begin{array}{cc} - 8 & 7 \\ - 7 & 6 \end{array})$ has determinant $1$ , and direct substitution gives $f ∣ M = g$ . Thus $f$ and $g$ are properly equivalent.

givenalgebra

2.1

Under Granville's positive-discriminant convention, a form of discriminant $d > 0$ is reduced when $0 < \sqrt{d} - b < 2 ∣ a ∣ < \sqrt{d} + b$ . Since $7 < \sqrt{60} < 8$ , one has $0 < \sqrt{60} - 6 < 2$ and $13 < \sqrt{60} + 6 < 14$ . Hence $0 < \sqrt{60} - 6 < 12 < \sqrt{60} + 6$ for $f$ and $0 < \sqrt{60} - 6 < 2 < \sqrt{60} + 6$ for $g$ , so both are reduced in that convention.

step 1.1algebra

3.1

The two reduced forms $f$ and $g$ are distinct, yet step 1.2 puts them in one proper-equivalence class. So the uniqueness statement [L1], which is true for positive-definite forms, does not extend to positive discriminant.

L1step 2.1step 1.2∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

Andrew Granville, Binary Quadratic Forms, Section 4.6 (standard reference, not scraped)