CorollaryStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-27

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.

Every real polynomial factors into linear and irreducible quadratic factors

Statement

Every nonzero polynomial $f \in R [x]$ can be written as a nonzero real scalar times a product of linear polynomials and irreducible quadratic polynomials.

Facts & Assumptions

Given: A nonzero polynomial $f \in R [x]$ .

[L1]

Every nonzero nonunit polynomial over a field factors into irreducible polynomials (Every nonzero nonunit polynomial over a field factors into irreducible polynomials).

[L2]

An irreducible polynomial in $R [x]$ has degree $1$ or $2$ (An irreducible polynomial in $R [x]$ has degree $1$ or $2$ ).

Proof

technique · direct

1.1

If $f$ is a nonzero constant, then it already has the required form: it is itself the nonzero scalar multiplying the empty product. Now assume that $f$ is a nonzero nonunit polynomial. By [L1], it factors as $f = u p_{1} \dots p_{r}$ with $u \in R^{\times}$ and each $p_{j}$ irreducible in $R [x]$ .

L1algebra

2.1

By [L2], each irreducible factor $p_{j}$ has degree $1$ or $2$ . Therefore each $p_{j}$ is either linear or an irreducible quadratic, so the factorization of step 1.1 is exactly the required one.

L2step 1.1

3.1

The constant and nonconstant cases together prove the statement for every nonzero polynomial in $R [x]$ .

step 1.1step 2.1∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

J. S. Milne, Fields and Galois Theory, v5.10, Chapter 5 (standard reference, not scraped)