ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

Second supplement in four residue classes modulo eight

Example

Let $ζ = ζ_{8} = e^{π i / 4}$ and $t = ζ + ζ^{- 1} = \sqrt{2}$ , where $\sqrt{2}$ denotes the positive real square root, so that $Q (\sqrt{2})$ is a quadratic subfield of $Q (ζ_{8})$ . For an odd prime $q$ , the arithmetic Frobenius of $q$ acts on $\sqrt{2}$ by ${Frob}_{q} (\sqrt{2}) = (\frac{2}{q}) \sqrt{2} = (- 1)^{(q^{2} - 1) / 8} \sqrt{2},$ with signs $+, -, -, +$ according as $q \equiv 1, 3, 5, 7 (m o d 8)$ .

Facts & Assumptions

Given: The primitive eighth root of unity $ζ = e^{π i / 4}$ , the element $t = ζ + ζ^{- 1}$ , and an odd prime $q$ .

[F1]

$ζ^{2} = ζ_{4}$ has order $4$ , so $t^{2} = 2$ . For every odd prime $q$ the arithmetic Frobenius of $q$ in $Q (ζ_{8})$ is the power map $ζ \mapsto ζ^{q}$ , so it sends $t = ζ + ζ^{- 1}$ to $ζ^{q} + ζ^{- q}$ , and ${Frob}_{q} (t) = (\frac{2}{q}) t = (- 1)^{(q^{2} - 1) / 8} t$ (Second supplement from Frobenius on Q(zeta_8), 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]

$ζ^{4} = - 1$ , hence $ζ^{7} = ζ^{- 1}$ , $ζ^{3} = - ζ^{- 1}$ and $ζ^{5} = ζ^{4} ζ = - ζ$ ; consequently, for an odd integer $m$ the value $ζ^{m}$ depends only on $m$ modulo $8$ and equals $ζ, - 1 \cdot ζ^{- 1}, - ζ, ζ^{- 1}$ for $m \equiv 1, 3, 5, 7 (m o d 8)$ respectively. [algebra]

[F3]

$(2 / q) = (- 1)^{(q^{2} - 1) / 8}$ , and the exponent $(q^{2} - 1) / 8$ is an integer for odd $q$ , even exactly when $q \equiv \pm 1 (m o d 8)$ (Second supplement from Frobenius on Q(zeta_8)).

Verification

technique · direct

1.1F2

For an odd prime $q$ the residue of $q$ modulo $8$ is one of $1, 3, 5, 7$ ; by [F2] the four corresponding values of $ζ^{q} + ζ^{- q}$ are $ζ + ζ^{- 1} = t$ , $- ζ^{- 1} - ζ = - t$ , $- ζ - ζ^{- 1} = - t$ and $ζ^{- 1} + ζ = t$ .

2.1F1step 1.1

Since ${Frob}_{q} (t) = ζ^{q} + ζ^{- q}$ is induced by the $q$ -th power map on $ζ$ , step 1.1 gives ${Frob}_{q} (t) = + t$ for $q \equiv 1, 7 (m o d 8)$ and ${Frob}_{q} (t) = - t$ for $q \equiv 3, 5 (m o d 8)$ .

3.1F1F3step 2.1∎

Comparing with [F1], $(\frac{2}{q}) = + 1$ for $q \equiv 1, 7 (m o d 8)$ and $(\frac{2}{q}) = - 1$ for $q \equiv 3, 5 (m o d 8)$ , matching the parity of $(q^{2} - 1) / 8$ described in [F3]; the signs in the order $q \equiv 1, 3, 5, 7$ are $+, -, -, +$ .

Remarks

A single sign computation covers all four classes. Only the residue of $q$ modulo $8$ enters, because $ζ^{4} = - 1$ makes the power map on $ζ$ depend on $q m o d 8$ .
$q = 2$ is excluded. The second supplement concerns odd $q$ ; the prime $q = 2$ is ramified in $Q (ζ_{8})$ and does not arise as a Frobenius prime of an unramified extension.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Jerry Shurman, Math 361 Ninth Lecture, sections 3-4 (standard reference, not scraped)
J. S. Milne, Algebraic Number Theory, Ch. 8, Example 8.18 (standard reference, not scraped)