Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: 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.

Reduction modulo 22 proves x3+17x+391x^3+17x+391 irreducible over Q\mathbb Q

Example

The polynomial f=x3+17x+391f=x^3+17x+391 is irreducible in Q[x]\mathbb Q[x].

Facts & Assumptions

Given: The primitive integer polynomial f=x3+17x+391f=x^3+17x+391.

[L1]

If a primitive integer polynomial has leading coefficient nonzero modulo a prime and its reduction is irreducible, then it is irreducible over Q\mathbb Q (Irreducibility after reduction modulo a prime implies irreducibility over Q\mathbb Q when the leading coefficient survives).

[L2]

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).

[L4]

An integer is prime when it exceeds 11 and has no positive divisors other than 11 and itself (Prime and composite integers: pp is prime when p>1p > 1 and its only positive divisors are 11 and pp).

[L6]

Integer absolute value is defined by sign cases (The absolute value a|a| of an integer).

[L8]

The integers form an ordered ring (The integers form a totally ordered ring).

[L9]

Natural numbers embed in the integers preserving arithmetic (The naturals embed in the integers).

[L11]

For prime pp, the ring Z/p\mathbb Z/p is a field (For every prime pp, the two operations on Z/p\mathbb{Z}/p make it a field).

Verification

technique · direct
1.1

Facts [L4] through [L10] show that 22 is prime, so [L11] makes Z/2\mathbb Z/2 a field. Using [L3], reduction gives fˉ=x3+x+1\bar f=x^3+x+1; its values at the only residues 00 and 11 are both 11, so [L2] makes fˉ\bar f irreducible.

givenL2L3L4L5L6L7L8L9L10L11algebra
2.1

The leading coefficient survives modulo 22, and ff is primitive because it is monic, so [L1] proves that ff is irreducible over Q\mathbb Q.

step 1.1L1

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 105 results over 28 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