PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (gpt-5.6-terra)audited 2026-08-28

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.

Integral Pell solutions form an abelian group

Statement

Fix a positive nonsquare integer $D$ , and identify an integral solution $(x, y)$ of Pell's equation with the element $x + y \sqrt{D} \in Z [\sqrt{D}]$ . Then the set $G_{D} : = {α \in Z [\sqrt{D}] : N_{D} (α) = 1}$ is an abelian group under multiplication in $Z [\sqrt{D}]$ .

Facts & Assumptions

Given: The set $G_{D} = {α \in Z [\sqrt{D}] : N_{D} (α) = 1}$ .

[F1]

For $α = x + y \sqrt{D} \in Z [\sqrt{D}]$ , the equality $N_{D} (α) = 1$ is exactly the equation $x^{2} - D y^{2} = 1$ , so $G_{D}$ is the set of integral Pell solutions written as elements of $Z [\sqrt{D}]$ (Pell's equation, The norm on the explicit order $Z [\sqrt{D}]$ ).

[F2]

The Pell norm is multiplicative: $N_{D} (α β) = N_{D} (α) N_{D} (β)$ for all $α, β \in Z [\sqrt{D}]$ (The Pell norm is multiplicative).

[F3]

In $Z [\sqrt{D}]$ , the product is

(x + y \sqrt{D}) (u + v \sqrt{D}) = (x u + D y v) + (x v + y u) \sqrt{D} .

(The norm on the explicit order $Z [\sqrt{D}]$ ).

Proof

technique · direct

1.1

The element $1 = 1 + 0 \sqrt{D}$ satisfies $N_{D} (1) = 1$ , so it lies in $G_{D}$ . If $α, β \in G_{D}$ , then [F2] gives $N_{D} (α β) = N_{D} (α) N_{D} (β) = 1,$ so $α β \in G_{D}$ .

F1F2givenalgebra

1.2

If $α = x + y \sqrt{D} \in G_{D}$ , then [F1] gives $x^{2} - D y^{2} = 1$ , hence $α (x - y \sqrt{D}) = x^{2} - D y^{2} = 1.$ Therefore $α^{- 1} = x - y \sqrt{D} \in G_{D}$ , since $N_{D} (x - y \sqrt{D}) = 1$ by [F1].

F1givenalgebra

2.1

Associativity is inherited from multiplication of real numbers, and [F3] is symmetric in $(x, y)$ and $(u, v)$ , so multiplication on $G_{D}$ is commutative. Together with steps 1.1 and 1.2, this proves that $G_{D}$ is an abelian group.

F3step 1.1step 1.2algebra∎

Depends on

Used by

All integral Pell solutions are ± ε_Dᵏ Corollary
Pell-equivalence for generalized solutions Definition
All positive Pell solutions are powers of the fundamental solution Theorem

Dependency tree · one level

3 results within one dependency step 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

Keith Conrad, Pell's Equation, I (standard reference, not scraped)
Peter Hackman, Elementary Number Theory (standard reference, not scraped)