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 subfield of Q(zeta_7)

Example

The unique intermediate field $Q \subseteq F \subseteq Q (ζ_{7})$ with $[F : Q] = 2$ is $F = Q (\sqrt{- 7}),$ namely the field generated by the quadratic Gauss sum $τ_{7}$ attached to a chosen primitive seventh root of unity.

Facts & Assumptions

Given: The odd prime $p = 7$ , a fixed primitive seventh root of unity $ζ = ζ_{7}$ , the Gauss sum $τ = τ_{7} = \sum_{a m o d 7} (a / 7) ζ^{a}$ attached to it, and $p^{*} = (- 1)^{(p - 1) / 2} p$ (Quadratic Gauss sum in a prime cyclotomic field, The cyclotomic extension $K (μ_{n})$ as a splitting field of $t^{n} - 1$ ).

[F1]

For every odd prime $p$ , the unique intermediate field $Q \subseteq F \subseteq Q (ζ_{p})$ with $[F : Q] = 2$ is $Q (τ_{p}) = Q (\sqrt{p^{*}})$ (Quadratic subfield generated by the Gauss sum).

[F2]

For every odd prime $p$ , $τ_{p}^{2} = p^{*}$ ; here in particular $τ^{2} = p^{*}$ (Square of the quadratic Gauss sum).

[F3]

$(7 - 1) / 2 = 3$ , so $p^{*} = (- 1)^{3} \cdot 7 = - 7$ . [arithmetic]

Verification

technique · direct

1.1F3

Substituting $p = 7$ into $p^{*} = (- 1)^{(p - 1) / 2} p$ gives $p^{*} = (- 1)^{3} \cdot 7 = - 7$ .

2.1step 1.1F1

By [F1] with $p = 7$ , the unique degree-two intermediate field of $Q (ζ_{7}) / Q$ is $Q (τ_{7}) = Q (\sqrt{p^{*}}) = Q (\sqrt{- 7})$ , where $τ_{7}$ is the Gauss sum attached to the chosen primitive root $ζ_{7}$ .

3.1F2step 1.1step 2.1∎

By [F2] with $p = 7$ , $τ^{2} = - 7$ , so $τ = \pm \sqrt{- 7}$ and the generator $Q (τ)$ is indeed $Q (\sqrt{- 7})$ , in agreement with the identification of step 2.1.

Remarks

The field is canonical, the generator is not. Replacing $ζ_{7}$ by another primitive seventh root multiplies $τ_{7}$ by a sign $\pm 1$ , so the element $τ_{7}$ is not canonical; the field $Q (\sqrt{- 7})$ it generates is, by the uniqueness clause of [F1]. This is the phenomenon recorded in the companion counterexample on the Gauss-sum sign.
Discriminant form. $- 7 \equiv 1 (m o d 4)$ , so $- 7$ is a fundamental discriminant. Since $Gal (Q (ζ_{7}) / Q) ≅ (Z / 7)^{\times}$ is cyclic of order $6$ , the field $Q (\sqrt{- 7})$ is the fixed field of its unique subgroup of order $3$ , and $Q (ζ_{7}) / Q (\sqrt{- 7})$ is a cyclic cubic extension.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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