Alphabeta Math
TheoremStatement: Literature-sourcedProof: Literature-sourcedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-11
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.

Division algorithm for polynomials over a field

Statement

Let FF be a field, let f∈F[x]f\in F[x], and let 0≠g∈F[x]0\ne g\in F[x]. There are unique polynomials q,r∈F[x]q,r\in F[x] such that

f=qg+r,r=0 or deg⁡r<deg⁡g.f=qg+r,\qquad r=0\ \text{or}\ \deg r<\deg g.

The statement includes f=0f=0 and nonzero constant divisors.

Facts & Assumptions

Given: A field FF, a polynomial ff, and a nonzero polynomial gg with leading coefficient cc.

[L1]

Division by a monic polynomial over a commutative ring has a unique quotient and degree-small remainder (Division by a monic polynomial over a commutative ring).

[L2]

Degrees add under multiplication of nonzero polynomials over a domain (Over an integral domain, degrees add under multiplication of nonzero polynomials).

[L3]

Every nonzero element of a field has a multiplicative inverse, and a field is commutative (Field).

[L4]

A nonzero polynomial has a nonzero leading coefficient; it is monic when that coefficient is 11 (Degree, leading coefficient and monic polynomial, with the zero polynomial having no degree).

Proof

technique · direct
1.1

By [L3] the coefficient cc has an inverse, and h=c−1gh=c^{-1}g is monic with the same degree as gg; [L1] gives unique Q,rQ,r with f=Qh+rf=Qh+r and r=0r=0 or deg⁡r<deg⁡g\deg r<\deg g, so q=c−1Qq=c^{-1}Q gives f=qg+rf=qg+r.

givenL1L3L4construct
2.1

If f=qg+r=q′g+r′f=qg+r=q'g+r', then (q−q′)g=r′−r(q-q')g=r'-r; unless q=q′q=q', [L2] makes the left side have degree at least deg⁡g\deg g, while the right side is zero or has degree below deg⁡g\deg g, so q=q′q=q' and then r=r′r=r'.

step 1.1L2L4algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 16 results over 6 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources