Alphabeta Math
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.

Properly equivalent reduced forms with the same leading coefficient are equal

Statement

Let f=(a,b,c) and g=(a,b,c) be reduced positive-definite binary quadratic forms. If f and g are properly equivalent, then f=g.

Facts & Assumptions

Given: Reduced positive-definite forms f=(a,b,c) and g=(a,b,c), and a matrix M=(pqrs)SL2(Z) with g=fM.

[F1]

Proper equivalence means g(x,y)=f(px+qy,rx+sy) (Proper equivalence of binary quadratic forms).

[F2]

Reduced forms satisfy bac and bac, with b0 whenever b=a or a=c, and similarly for b (Reduced positive-definite binary quadratic forms).

[F3]

The discriminant of (u,v,w) is v24uw (The discriminant of a binary quadratic form).

Proof

technique · direct
1.1

The leading coefficient of g is g(1,0)=f(p,r)=ap2+bpr+cr2, and because bac one has g(1,0)a(p2pr+r2)a. Since g has leading coefficient exactly a, equality holds throughout.

F1F2algebra
2.1

Equality in step 1.1 forces p2pr+r2=1, so (p,r) is one of (1,0), (0,1), or (1,1).

step 1.1algebra
3.1

If (p,r)=(1,0), then r=0 and p=±1. The determinant condition gives s=p and M=(pq0p). The transformed middle coefficient is b=b+2aq when p=1 and b=b2aq when p=1, so ba and ba force q=0 unless b=a and b=b. But the boundary rule in [F2] forbids b=a for a reduced form, so q=0, hence b=b and c=c.

F1F2step 2.1algebra
3.2

If (p,r)=(0,1), then p=0 and r=±1. Equality in step 1.1 gives c=a, so reducedness of f yields 0ba. The determinant condition gives q=r, so M=(0rrs), and direct substitution gives g=(a,b+2ars,abrs+as2). Since g is reduced, b+2arsa. If s=0, then g=(a,b,a), and reducedness of g with a=c=a forces b0; together with b0 this gives b=0, hence g=f. If s0, then the same bound implies 2asba, so s=1 and b=a; because 0ba, this means b=a, and the sign of b+2ars shows rs=1. Then g=(a,a,a)=f.

F1F2step 1.1step 2.1algebra
3.3

If (p,r)=(1,1), equality in step 1.1 forces c=a and b=a. By reducedness, b=a. Replacing M by M if necessary does not change the substitution, so we may assume (p,r)=(1,1). Then s+q=1, and the transformed middle coefficient is b=a(2q1). Since ba, one has q=0 or q=1; reducedness excludes b=a, so q=1 and b=a. The discriminant identity b24ac=b24ac then gives c=a=c, so again g=f.

F1F2F3step 1.1step 2.1algebra
4.1

The three cases of step 2.1 are exhaustive, and each yields g=f. Therefore properly equivalent reduced forms with the same leading coefficient are equal.

step 3.1step 3.2step 3.3

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