ExampleConstruction: Literature-sourcedVerification: Literature-sourcedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

No nontrivial everywhere unramified number field over Q

Example

Assume the Axiom of Choice. A finite number field $K \neq Q$ cannot be unramified at every finite rational prime. Indeed, if $K$ were unramified at every rational prime, the ramification-discriminant criterion would leave $d_{K}$ a nonzero integer with no prime divisor, so $∣ d_{K} ∣ = 1$ ; but every field of degree $n > 1$ has $∣ d_{K} ∣ > 1$ . The statement concerns finite primes only, and no archimedean convention is used.

Facts & Assumptions

Given: The Axiom of Choice, a number field $K$ with $K \neq Q$ , so that $n = [K : Q] > 1$ , and the discriminant $d_{K}$ .

[F1]

A rational prime $p$ ramifies in $K / Q$ if and only if $p ∣ d_{K}$ (Ramification is detected by the number-field discriminant).

[F2]

Every finite number field $K$ with $[K : Q] > 1$ has a rational prime that ramifies in $K$ (Every nontrivial number field has a ramified finite prime).

[F3]

For $n > 1$ one has $∣ d_{K} ∣ > 1$ (Nontrivial number fields have discriminant of absolute value greater than one).

[F4]

$d_{K}$ is a nonzero signed integer (Number-field discriminant is well-defined and nonzero).

[F5]

Every integer greater than $1$ has a prime divisor (Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime).

[F6]

A prime is unramified in an extension when all its ramification indices are $1$ , and ramified otherwise; for $K / Q$ the relevant primes of $Z$ are the rational primes (Splitting and ramification terminology).

Proof

1.1F4given

By [F4] the discriminant $d_{K}$ is a nonzero integer.

2.1F1F6step 1.1

If $K$ is unramified at every rational prime, then no rational prime divides $d_{K}$ : for if $p ∣ d_{K}$ , then [F1] makes $p$ ramified in $K$ , and [F6] exhibits a ramification index exceeding $1$ at $p$ , contrary to the hypothesis.

2.2F4F5step 1.1

Conversely, if no rational prime divides $d_{K}$ , then $∣ d_{K} ∣ = 1$ : otherwise $∣ d_{K} ∣ > 1$ and [F5] would produce a rational prime dividing $∣ d_{K} ∣$ , hence dividing $d_{K}$ , and $d_{K} \neq 0$ by step 1.1 leaves $∣ d_{K} ∣ = 1$ .

3.1F1step 2.1step 2.2

Equivalence: $K$ is unramified at every rational prime if and only if $∣ d_{K} ∣ = 1$ . Indeed, unramified everywhere gives no prime divisor of $d_{K}$ by step 2.1 and then $∣ d_{K} ∣ = 1$ by step 2.2; conversely, if $∣ d_{K} ∣ = 1$ then no rational prime divides $d_{K}$ , so no rational prime ramifies by [F1].

4.1F2F3step 3.1

But $n > 1$ , so [F3] gives $∣ d_{K} ∣ > 1$ , contradicting the equivalence in step 3.1; equivalently, [F2] directly produces a ramified rational prime.

5.1F1F2step 3.1step 4.1∎

Therefore no finite number field $K \neq Q$ is unramified at every finite rational prime. The argument uses only finite primes: $d_{K}$ is the determinant of the trace pairing of an integral basis, the criterion [F1] concerns rational primes, and no archimedean place enters; correspondingly $d_{Q} = 1$ and $Q$ itself has no ramified primes.

Remarks

The example is the contrapositive form of the ramification criterion: an integer discriminant with no prime divisor must be $\pm 1$ , and $\pm 1$ is impossible for a field of degree greater than one. The hypothesis $K \neq Q$ is essential, since $d_{Q} = 1$ and $Q$ has no ramified finite prime. The phrase "every finite rational prime" is deliberate: the criterion and the discriminant are statements about finite primes, and no claim about archimedean places is made or needed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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, Algebraic Number Theory v3.08 (standard reference, not scraped)
Brian Conrad and Aaron Landesman, Math 154 Algebraic Number Theory (standard reference, not scraped)