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

Every Pell equation has a positive nontrivial integral solution

Statement

For every positive nonsquare integer D, Pell's equation x2−Dy2=1 has a positive nontrivial integral solution.

Facts & Assumptions

Given: A positive nonsquare integer D.

[F1]

If a0=⌊D⌋, then D=[a0;a1,…,aℓ−1,2a0‾] for some ℓ≥1, and the returned state satisfies Qℓ=1 (The continued fraction of D has symmetric period ending in 2a0).

[F2]

The convergents of D satisfy pn2−Dqn2=(−1)n+1Qn+1. (Convergents to D satisfy the norm identity).

[F3]

The Pell norm is multiplicative on Z[D] (The Pell norm is multiplicative).

Proof

technique · direct
1.1F1F2givenalgebra

Let ℓ be the period length from [F1]. Applying [F2] at n=ℓ−1 and using Qℓ=1 gives pℓ−12−Dqℓ−12=(−1)ℓ.

2.1step 1.1algebra

If ℓ is even, step 1.1 already gives a norm-one solution. Since qℓ−1>0 for every convergent denominator and pℓ−12=Dqℓ−12+1, one has pℓ−1>0 and qℓ−1>0, so (pℓ−1,qℓ−1) is a positive nontrivial solution.

3.1F3step 1.1algebra

If ℓ is odd, step 1.1 gives pℓ−12−Dqℓ−12=−1. Put α:=pℓ−1+qℓ−1D. Then pℓ−1>0 and qℓ−1>0 as in step 2.1, and [F3] gives ND(α2)=ND(α)2=(−1)2=1. Explicitly, α2=(pℓ−12+Dqℓ−12)+2pℓ−1qℓ−1D, so α2 gives a positive nontrivial integral solution of Pell's equation.

4.1step 2.1step 3.1∎

Either step 2.1 or step 3.1 supplies the required positive nontrivial solution.

Depends on

Used by

Dependency tree · two levels

9 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