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

Quadratic Gauss sum at p=3

Example

For the standard complex primitive third root of unity $ζ_{3} = e^{2 π i / 3}$ , the quadratic Gauss sum is $τ_{3} = ζ_{3} - ζ_{3}^{2} = i \sqrt{3}, τ_{3}^{2} = - 3.$

Facts & Assumptions

Given: The prime $p = 3$ , the primitive third root of unity $ζ = ζ_{3} = e^{2 π i / 3}$ , and the Gauss sum $τ = τ_{3} = \sum_{a m o d 3} (a / 3) ζ^{a}$ .

[L1]

$(1 / 3) = 1$ and $(2 / 3) = - 1$ , so $τ = (1 / 3) ζ + (2 / 3) ζ^{2} = ζ - ζ^{2}$ (Quadratic Gauss sum in a prime cyclotomic field, The Legendre symbol, including its zero value).

[L2]

For every odd prime $p$ , $τ_{p}^{2} = p^{*} = (- 1)^{(p - 1) / 2} p$ , so here $τ^{2} = - 3$ (Square of the quadratic Gauss sum).

[L3]

The third roots of unity are $ζ^{k} = \exp (2 π i k / 3)$ for $k = 0, 1, 2$ , so $ζ = \exp (2 π i / 3)$ and $ζ^{3} = 1$ (The $n$ -th roots of a complex number and the $n$ distinct roots of unity for every $n \geq 1$ ).

[L4]

Euler's formula $\exp (i θ) = \cos θ + i \sin θ$ holds for real $θ$ (Euler's formula: $\exp (i θ) = \cos θ + i \sin θ$ for every real $θ$ ), and $\sin (- x) = - \sin x$ , $\sin (π - x) = \sin x$ for real $x$ (Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions); moreover $\sin x > 0$ for $0 < x < π$ (Pi is the first positive zero of sine).

[L5]

$∣ \exp (i θ) ∣ = 1$ for real $θ$ , so $\overline{ζ} = ζ^{- 1}$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ ).

Verification

technique · direct

1.1L1

Substituting the Legendre values, $τ = ζ - ζ^{2}$ .

2.1L3L4L5step 1.1

Since $ζ^{3} = 1$ we have $ζ^{2} = ζ^{- 1}$ , and by [L5] also $ζ^{2} = \overline{ζ}$ ; thus $τ = ζ - ζ^{- 1} = \exp (2 π i / 3) - \exp (- 2 π i / 3) = 2 i \sin (2 π / 3) = 2 i \sin (π / 3)$ , using Euler's formula and the reflection identity.

3.1L2L4step 2.1

From step 2.1, $τ^{2} = (2 i \sin (π / 3))^{2} = - 4 \sin^{2} (π / 3)$ , while [L2] gives $τ^{2} = - 3$ ; hence $\sin^{2} (π / 3) = 3 / 4$ , and $\sin (π / 3) > 0$ because $0 < π / 3 < π$ , so $\sin (π / 3) = \sqrt{3} / 2$ .

4.1L2step 2.1step 3.1∎

Substituting back, $τ = 2 i \cdot (\sqrt{3} / 2) = i \sqrt{3}$ , and $τ^{2} = (i \sqrt{3})^{2} = - 3$ , in agreement with the general square formula.

Remarks

The choice of root matters for the sign. With $ζ_{3} = e^{2 π i / 3}$ the sum is $+ i \sqrt{3}$ ; replacing $ζ_{3}$ by $ζ_{3}^{2}$ multiplies $τ_{3}$ by $(2 / 3) = - 1$ and gives $- i \sqrt{3}$ . The square $- 3$ is the same in both cases.

Depends on

Used by

The sign of a quadratic Gauss sum needs a chosen primitive root Counterexample

Dependency tree · two levels

40 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 2-3 (standard reference, not scraped)
J. S. Milne, Algebraic Number Theory, Ch. 8, Example 8.19 (standard reference, not scraped)