Alphabeta MathHow 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.
Reduction modulo proves irreducible over
Example
The polynomial is irreducible in .
Facts & Assumptions
Given: The primitive integer polynomial .
If a primitive integer polynomial has leading coefficient nonzero modulo a prime and its reduction is irreducible, then it is irreducible over (Irreducibility after reduction modulo a prime implies irreducibility over when the leading coefficient survives).
A cubic over a field is irreducible exactly when it has no root in the field (A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field).
The ring is the quotient (For every , the congruence-class ring is the quotient ring ).
An integer is prime when it exceeds and has no positive divisors other than and itself (Prime and composite integers: is prime when and its only positive divisors are and ).
Integer divisors of a nonzero integer are bounded in absolute value (If and then and ; hence the set of divisors of a nonzero integer is bounded above by ).
Integer absolute value is defined by sign cases (The absolute value of an integer).
Integer absolute value is nonnegative and detects zero (Absolute value in : ; exactly when ; ; ; ; and exactly when ).
The integers form an ordered ring (The integers form a totally ordered ring).
Natural numbers embed in the integers preserving arithmetic (The naturals embed in the integers).
The natural order is discrete (Discreteness: is the immediate successor).
For prime , the ring is a field (For every prime , the two operations on make it a field).
Verification
Facts [L4] through [L10] show that is prime, so [L11] makes a field. Using [L3], reduction gives ; its values at the only residues and are both , so [L2] makes irreducible.
The leading coefficient survives modulo , and is primitive because it is monic, so [L1] proves that is irreducible over .
Depends on
- Irreducibility after reduction modulo a prime implies irreducibility over $\mathbb Q$ when the leading coefficient survives
- A polynomial of degree two or three over a field is irreducible exactly when it has no root in the field
- For every $n\in\mathbb N$, the congruence-class ring $\mathbb Z/n$ is the quotient ring $\mathbb Z/n\mathbb Z$
- For every prime $p$, the two operations on $\mathbb{Z}/p$ make it a field
- Prime and composite integers: $p$ is prime when $p > 1$ and its only positive divisors are $1$ and $p$
- If $d \mid a$ and $a \ne 0$ then $d \ne 0$ and $|d| \le |a|$; hence the set of divisors of a nonzero integer is bounded above by $|a|$
- The absolute value $|a|$ of an integer
- Absolute value in $\mathbb{Z}$: $|a| \ge 0$; $|a| = 0$ exactly when $a = 0$; $|-a| = |a|$; $|ab| = |a|\,|b|$; $-|a| \le a \le |a|$; and $|a| \le c$ exactly when $-c \le a \le c$
- The integers form a totally ordered ring
- The naturals embed in the integers
- Discreteness: $\sigma(n)$ is the immediate successor
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
51 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
- Neil Donaldson, Math 120B Notes, example after Theorem 23.13 (standard reference, not scraped)