Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedprecheck passjudge pass (gpt-5.6-terra)audited 2026-09-05
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.

Quadratic forms of dimension at least three over odd finite fields are isotropic

Statement

Let F be a finite field of odd order, and let q be a quadratic form on an F-vector space of dimension at least 3. Then q is isotropic.

Facts & Assumptions

Given: A finite field F of odd order and a quadratic form q on an n-dimensional F-vector space with n3.

[L2]

The multiplicative group of a finite field is cyclic (The multiplicative group Fq× of a finite field is cyclic).

[L3]

A finite field has finite order (Finite fields and their order); in the present statement that order is assumed odd.

Proof

technique · direct
1.1

By [L1], after choosing a basis we may write q(x1,,xn)=a1x12++anxn2. If some ai=0, then the corresponding basis vector is a nonzero isotropic vector. So we may assume a1,a2,a30 and restrict to the ternary subform a1x2+a2y2+a3z2.

L1givencases
2.1

Let Q={u2:uF} be the set of square classes including 0. By [L2] and [L3], F× has even order, so the nonzero squares form an index-two subgroup and Q=(F+1)/2. The sets a1Q and a3a2Q therefore each have more than half the elements of F, so they intersect. Hence there exist x,yF with a1x2=a3a2y2, and then (x,y,1) is a nonzero isotropic vector for the ternary subform and therefore for q.

L2L3step 1.1algebra

Depends on

Used by

Dependency tree · two levels

12 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