Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26
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.

Additive Hilbert 90: trace zero is the image of α↦α−σ(α)

Statement

Let K/F be a finite cyclic extension of degree n with Gal⁡(K/F)=⟨σ⟩. For b∈K, the following are equivalent:

  1. Tr⁡K/F(b)=0.
  2. There exists α∈K with b=α−σ(α).

Facts & Assumptions

Given: A finite cyclic extension K/F of degree n, a generator σ of its Galois group, and an element b∈K.

[F1]

A cyclic extension is finite Galois and therefore finite separable (A cyclic extension is a finite Galois extension with cyclic Galois group).

[L1]

In a finite separable extension, the trace map is surjective (The trace map of a finite separable extension is surjective).

Proof

technique · direct
1.1F1algebra

For the forward direction from 2 to 1, suppose b=α−σ(α). Summing the conjugates gives Tr⁡K/F(b)=∑i=0n−1σi(α−σ(α))=∑i=0n−1(σi(α)−σi+1(α))=0, again by telescoping and σn=1.

1.2F1L1choose

For the converse, assume Tr⁡K/F(b)=0. By [F1] and [L1], choose c∈K with Tr⁡K/F(c)=1. Define α:=∑i=0n−1(∑j=0i−1σj(b))σi(c), where the inner sum is 0 for i=0.

2.1step 1.2algebra

Put si=∑j=0i−1σj(b), so s0=0, sn=Tr⁡K/F(b)=0, and si=b+σ(si−1) for 1≤i≤n−1, while 0=sn=b+σ(sn−1). Applying σ to the coefficients as well gives σ(α)=∑i=0n−1σ(si)σi+1(c)=σ(sn−1)c+∑i=1n−1σ(si−1)σi(c). Therefore every coefficient of α−σ(α) is b, so α−σ(α)=b∑i=0n−1σi(c)=b Tr⁡K/F(c)=b.

3.1step 1.1step 2.1∎

Steps 1.1 and 2.1 prove the equivalence.

Remarks

  • This is the additive engine behind Artin-Schreier theory. The next theorem applies it to the trace-zero element −1 in characteristic p.

Depends on

Used by

Dependency tree · two levels

4 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