Alphabeta Math
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.

Frobenius restriction for p=5 and q=3

Example

In Q(ζ5) the arithmetic Frobenius of the prime 3 acts on the quadratic subfield Q(5) by Frob⁡3(5)=−5, that is, nontrivially; the two Legendre symbols agree, (35)=(53)=−1.

Facts & Assumptions

Given: The distinct odd primes p=5 and q=3, a fixed primitive fifth root of unity ζ5, the Gauss sum τ5 attached to it, and p∗=(−1)(p−1)/2p (Quadratic Gauss sum in a prime cyclotomic field).

[F1]

For distinct odd primes p,q, the arithmetic Frobenius of q in Q(ζp) acts on the quadratic subfield Q(p∗) by τp↦(p∗q)τp, and (p∗q)=(qp) (Quadratic reciprocity as a Frobenius restriction identity).

[F2]

For p=5 one has p∗=(−1)2⋅5=5 and τ52=5, so τ5=ε5 for some ε∈{1,−1} (Square of the quadratic Gauss sum). For the standard complex root ζ5=e2πi/5 one has ε=1; moreover Q(τ5)=Q(5) is the unique quadratic subfield of Q(ζ5) (Quadratic Gauss sum at p=5, Quadratic subfield generated by the Gauss sum).

[F3]

Legendre symbols: (35)=−1 because the nonzero squares modulo 5 are 1,4 and 3 is not among them, and (53)=(23)=−1 because 5≡2(mod3) and the only nonzero square modulo 3 is 1 (The Legendre symbol, including its zero value, Quadratic residues and nonresidues modulo an integer).

Verification

technique · direct
1.1F2

For p=5 the quadratic subfield is Q(p∗)=Q(5)=Q(τ5), with τ5=ε5≠0 for some rational sign ε∈{1,−1}.

1.2F3

(35)=−1 and (53)=(23)=−1.

2.1F1step 1.1step 1.2

By [F1] with p=5, q=3, the arithmetic Frobenius satisfies Frob⁡3(τ5)=(53)τ5=−τ5. Since it fixes ε∈Q, step 1.1 gives εFrob⁡3(5)=−ε5, hence Frob⁡3(5)=−5. The restriction identity gives (53)=(35)=−1.

3.1step 1.1step 2.1∎

Since τ5≠0, one has Frob⁡3(τ5)=−τ5≠τ5, so the arithmetic Frobenius of 3 acts nontrivially on Q(5): it is the nontrivial element of Gal⁡(Q(5)/Q), and the two Legendre symbols both equal −1, in agreement with the reciprocity law (3/5)(5/3)=(−1)2⋅1=1.

Remarks

  • Nontrivial restriction means non-splitting. The Frobenius of 3 restricting nontrivially to Q(5) is the Frobenius form of the statement that 3 does not split in Q(5), equivalently (53)=−1.
  • Reciprocity check. The equality (53)=(35) is the special case p=5, q=3 of Quadratic reciprocity as a Frobenius restriction identity; note (p−1)(q−1)/4=2⋅1=2 is even, so the general reciprocity sign is +1, as displayed.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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