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.
Properly equivalent reduced forms with the same leading coefficient are equal
Statement
Let and be reduced positive-definite binary quadratic forms. If and are properly equivalent, then .
Facts & Assumptions
Given: Reduced positive-definite forms and , and a matrix with .
Proper equivalence means (Proper equivalence of binary quadratic forms).
Reduced forms satisfy and , with whenever or , and similarly for (Reduced positive-definite binary quadratic forms).
The discriminant of is (The discriminant of a binary quadratic form).
Proof
The leading coefficient of is , and because one has . Since has leading coefficient exactly , equality holds throughout.
Equality in step 1.1 forces , so is one of , , or .
If , then and . The determinant condition gives and . The transformed middle coefficient is when and when , so and force unless and . But the boundary rule in [F2] forbids for a reduced form, so , hence and .
If , then and . Equality in step 1.1 gives , so reducedness of yields . The determinant condition gives , so , and direct substitution gives . Since is reduced, . If , then , and reducedness of with forces ; together with this gives , hence . If , then the same bound implies , so and ; because , this means , and the sign of shows . Then .
If , equality in step 1.1 forces and . By reducedness, . Replacing by if necessary does not change the substitution, so we may assume . Then , and the transformed middle coefficient is . Since , one has or ; reducedness excludes , so and . The discriminant identity then gives , so again .
The three cases of step 2.1 are exhaustive, and each yields . Therefore properly equivalent reduced forms with the same leading coefficient are equal.
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, Theorem 9.3.2 (standard reference, not scraped)
- Andrew Granville, Binary Quadratic Forms, Exercise 4.1f(b) (standard reference, not scraped)