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 be a finite field of odd order, and let be a quadratic form on an -vector space of dimension at least . Then is isotropic.
Facts & Assumptions
Given: A finite field of odd order and a quadratic form on an -dimensional -vector space with .
Over characteristic not , a quadratic form diagonalizes (Over a field of characteristic not , every quadratic form has diagonal coordinates ).
The multiplicative group of a finite field is cyclic (The multiplicative group of a finite field is cyclic).
A finite field has finite order (Finite fields and their order); in the present statement that order is assumed odd.
Proof
By [L1], after choosing a basis we may write . If some , then the corresponding basis vector is a nonzero isotropic vector. So we may assume and restrict to the ternary subform .
Let be the set of square classes including . By [L2] and [L3], has even order, so the nonzero squares form an index-two subgroup and . The sets and therefore each have more than half the elements of , so they intersect. Hence there exist with , and then is a nonzero isotropic vector for the ternary subform and therefore for .
Depends on
- Finite fields and their order
- The multiplicative group $\mathbb F_q^\times$ of a finite field is cyclic
- A quadratic form $q$ in arbitrary characteristic and its polar form $b_q(u,v)=q(u+v)-q(u)-q(v)$
- Over a field of characteristic not $2$, every quadratic form has diagonal coordinates $q(x)=a_1x_1^2+\cdots+a_nx_n^2$
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
- Andrew V. Sutherland, 18.782 Lecture 11 (standard reference, not scraped)
- Sam Raskin, Introduction to the Arithmetic Theory of Quadratic Forms, section 4.5 (standard reference, not scraped)