CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

First supplement from Frobenius on Q(i)

Statement

For every odd prime $q$ , the arithmetic Frobenius of $q$ in the quadratic field $Q (i) = Q (ζ_{4})$ sends $i$ to ${Frob}_{q} (i) = i^{q} = (- 1)^{(q - 1) / 2} i,$ so it acts on $Q (i)$ by the quadratic sign $(- 1 / q) = (- 1)^{(q - 1) / 2}$ .

Facts & Assumptions

Given: An odd prime $q$ , the element $i = ζ_{4}$ , a primitive fourth root of unity, and the field $K = Q (i) = Q (ζ_{4})$ of degree $2$ over $Q$ .

[F1]

The index $f = 4$ is reduced, and $q ∤ 4$ ; hence the arithmetic Frobenius of $q$ in $Q (ζ_{4}) / Q$ is the power map $σ_{q} (ζ_{4}) = ζ_{4}^{q}$ (Arithmetic Frobenius is the power map in an unramified cyclotomic field, The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ).

[F2]

$O_{Q (i)} = Z [i]$ , and $i^{2} = - 1$ , so $i^{q} = i (i^{2})^{(q - 1) / 2} = (- 1)^{(q - 1) / 2} i$ for odd $q$ (Ring of integers of every cyclotomic field).

[F3]

Euler's criterion: for every integer $a$ and odd prime $q$ , $(a / q) \equiv a^{(q - 1) / 2} (m o d q)$ (Euler's criterion: $(a / p) \equiv a^{(p - 1) / 2} (m o d p)$ , The Legendre symbol, including its zero value); the Legendre symbol satisfies $(a / q) \in {- 1, 0, 1}$ .

Proof

technique · direct

1.1F1F2

By [F1] the Frobenius of $q$ acts on $K$ as the power map on $ζ_{4} = i$ , and by [F2] this is ${Frob}_{q} (i) = i^{q} = (- 1)^{(q - 1) / 2} i$ .

1.2F3

By Euler's criterion with $a = - 1$ , $(- 1 / q) \equiv (- 1)^{(q - 1) / 2} (m o d q)$ ; both $(- 1 / q)$ and $(- 1)^{(q - 1) / 2}$ are elements of ${- 1, 1}$ , so their difference is $0$ or $\pm 2$ , and a multiple of the odd prime $q$ ; hence the difference is $0$ and $(- 1 / q) = (- 1)^{(q - 1) / 2}$ .

2.1step 1.1step 1.2∎

Therefore the arithmetic Frobenius acts on $i$ by multiplication by the quadratic sign $(- 1 / q)$ , that is ${Frob}_{q} (i) = (- 1 / q) i$ .

Remarks

Independence from the earlier supplement. The sign is computed here from the power map and Euler's criterion; the published first-supplement theorem is not used as a supplier, so no circularity arises with the quadratic reciprocity corollary that consumes this item.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

38 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, Ch. 6, Remark 6.3(a) and Ch. 8 (standard reference, not scraped)
Conrad-Landesman, Math 154 Algebraic Number Theory, Ch. 12 (standard reference, not scraped)