ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-30

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.

Finite-field normalization needs the weight trick

Example

Let $k = F_{q}$ and

f (x, y) = x^{q} y - x y^{q} .

Then no substitution $x \mapsto x + a y$ with $a \in F_{q}$ makes $f$ monic in $y$ , but the weight substitution $x \mapsto x + y^{N}$ with $N > q$ does.

Facts & Assumptions

Given: The finite field $F_{q}$ and the polynomial $f (x, y) = x^{q} y - x y^{q}$ .

[L1]

Rapidly increasing exponent substitutions isolate a unique highest $x_{n}$ -term (Rapidly increasing power substitutions isolate one highest x_n-term).

Verification

technique · direct

1.1

The highest homogeneous part of $f$ is $f$ itself. For any $a \in F_{q}$ , $f (a, 1) = a^{q} - a = 0,$ so the infinite-field linear-change argument cannot choose a scalar $a \in F_{q}$ with nonzero leading coefficient.

given

2.1

Now substitute $x \mapsto x + y^{N}$ with $N > q$ . Because $q$ is a power of the characteristic of $F_{q}$ , the Frobenius identity gives $(x + y^{N})^{q} = x^{q} + y^{N q}$ . Hence $f (x + y^{N}, y) = x^{q} y + y^{N q + 1} - x y^{q} - y^{N + q} .$ Because $N q + 1 > N + q$ , the term $y^{N q + 1}$ is the unique highest power of $y$ . Therefore the transformed polynomial is already monic in $y$ , exactly as [L1] predicts.

L1step 1.1∎

Depends on

Rapidly increasing power substitutions isolate one highest x_n-term

Used by

Nothing in the library uses this result yet.

Dependency tree · one level

1 result within one dependency step 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

Allen B. Altman and Steven L. Kleiman, A Term of Commutative Algebra, 13th ed., Exercise (15.2) (standard reference, not scraped)