ExampleConstruction: Literature-sourcedVerification: AI-adaptedSession-authored (Fable 5 assisted)precheck 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.

Hilbert 90 for $Q (i) / Q$ recovers the rational parametrization of the unit circle

Example

Let $K = Q (i)$ over $Q$ , with Galois generator $σ (a + b i) = a - b i$ . Then every rational point $(x, y)$ on

$x^{2} + y^{2} = 1$

with $x \neq - 1$ has the form

$x = \frac{1 - t^{2}}{1 + t^{2}}, y = \frac{2 t}{1 + t^{2}}$

for some $t \in Q$ . Equivalently, every primitive Pythagorean triple is obtained from this parametrization after clearing denominators.

Facts & Assumptions

Given: The quadratic extension $K / Q$ and its nontrivial automorphism $σ (a + b i) = a - b i$ .

[L1]

In a finite cyclic extension, norm one is equivalent to being of the form $β / σ (β)$ (Hilbert's theorem 90 for a finite cyclic extension).

Verification

technique · direct

1.1

If $(x, y) \in Q^{2}$ satisfies $x^{2} + y^{2} = 1$ , then $α = x + y i \in K^{\times}$ has norm one. By [L1], there is $β = u + v i \in K^{\times}$ with $x + y i = \frac{β}{σ (β)} = \frac{u + v i}{u - v i} = \frac{(u + v i)^{2}}{u^{2} + v^{2}} = \frac{u^{2} - v^{2}}{u^{2} + v^{2}} + \frac{2 u v}{u^{2} + v^{2}} i .$ If $u = 0$ then $x = - 1$ , excluded in the statement. So with $t = v / u \in Q$ one gets $x = \frac{1 - t^{2}}{1 + t^{2}}, y = \frac{2 t}{1 + t^{2}} .$

L1algebra

2.1

Conversely, every rational $t$ gives ${(\frac{1 - t^{2}}{1 + t^{2}})}^{2} + {(\frac{2 t}{1 + t^{2}})}^{2} = 1,$ so the displayed formula indeed parametrizes rational points on the unit circle. Clearing denominators gives the classical Pythagorean triple formulas.

step 1.1algebra∎

Depends on

Hilbert's theorem 90 for a finite cyclic extension

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

5 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

J. S. Milne, Fields and Galois Theory, v5.10, Exercise 5-2 (standard reference, not scraped)
S. R. Ghorpade, Lectures on Field Theory and Ramification Theory, Section 1.3 (standard reference, not scraped)

Hilbert 90 for Q(i)/QQ(i)/Q recovers the rational parametrization of the unit circle