LemmaStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 2026-08-17

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.

A nonsingular square root lifts uniquely by one odd-prime-power step

Statement

Let $p$ be an odd prime, let $k \geq 1$ , and let $a, x_{k} \in Z$ satisfy $p ∤ a$ and $x_{k}^{2} \equiv a (m o d p^{k})$ . Then there is a unique class $t (m o d p)$ such that $(x_{k} + t p^{k})^{2} \equiv a (m o d p^{k + 1})$ .

Equivalently, the root class of $x_{k}$ modulo $p^{k}$ has exactly one lift to a root class modulo $p^{k + 1}$ .

Facts & Assumptions

Given: An odd prime $p$ , an integer $k \geq 1$ , and integers $a, x_{k}$ with $p ∤ a$ and $x_{k}^{2} \equiv a (m o d p^{k})$ .

[L1]

If $d = \gcd (c, n)$ , then $c t \equiv b (m o d n)$ is soluble exactly when $d ∣ b$ , and when soluble it has exactly $d$ solution classes modulo $n$ (For $n \geq 1$ , $a x \equiv b (m o d n)$ is solvable exactly when $\gcd (a, n) ∣ b$ , and then has exactly $\gcd (a, n)$ solution classes modulo $n$ ).

[L2]

If a prime $p$ divides a product $u v$ , then $p ∣ u$ or $p ∣ v$ (Euclid's lemma: if $p$ is prime and $p ∣ a b$ then $p ∣ a$ or $p ∣ b$ ).

[L3]

If a prime $p$ does not divide an integer $u$ , then $\gcd (p, u) = 1$ (For a prime $p$ and any integer $a$ , $\gcd (p, a)$ is $p$ when $p ∣ a$ and $1$ otherwise; so $p ∤ a$ makes $p$ and $a$ coprime).

Proof

technique · direct

1.1

Reducing the given congruence modulo $p$ shows that $p ∣ x_{k}$ would force $p ∣ a$ , contrary to the hypothesis. If $p ∣ 2 x_{k}$ , [L2] would give $p ∣ 2$ or $p ∣ x_{k}$ ; both are impossible because $p$ is odd. Hence $p ∤ 2 x_{k}$ , and [L3] gives $\gcd (2 x_{k}, p) = 1$ .

L2L3given

2.1

Write $x_{k}^{2} - a = c p^{k}$ . Every class modulo $p^{k + 1}$ reducing to $x_{k}$ modulo $p^{k}$ has a unique form $x_{k} + t p^{k}$ with $t$ modulo $p$ , and expansion gives $(x_{k} + t p^{k})^{2} - a = p^{k} (c + 2 x_{k} t + t^{2} p^{k})$ . Since $k \geq 1$ , the lift is a root modulo $p^{k + 1}$ exactly when $2 x_{k} t \equiv - c (m o d p)$ . By step 1.1 and [L1], this linear congruence has exactly one solution class $t$ modulo $p$ .

step 1.1L1algebra∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 67 results over 20 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

A. Gorodnik, Number Theory, Lecture 7, §1 (standard reference, not scraped)
P. Hackman, Elementary Number Theory, §B.VII (standard reference, not scraped)