TheoremStatement: Literature-sourcedProof: 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 unit is a square modulo $n$ exactly when it is a square at every prime-power factor

Statement

Let $n \geq 1$ and let $[a]_{n} \in (Z / n)^{\times}$ . A unit is a square modulo $n$ if and only if it is a square modulo every prime-power factor of $n$ .

Equivalently, for every odd prime $p ∣ n$ one must have $(a / p) = 1$ ; for the factor $2^{e}$ , there is no additional condition when $e \leq 1$ , one needs $a \equiv 1 (m o d 4)$ when $e = 2$ , and one needs $a \equiv 1 (m o d 8)$ when $e \geq 3$ . At $n = 1$ , the unique unit class is a square.

Facts & Assumptions

Given: A positive integer $n$ and a unit class $[a]_{n}$ .

[L1]

For an odd prime $p$ , $k \geq 1$ , and $p ∤ a$ , the congruence $x^{2} \equiv a (m o d p^{k})$ is soluble if and only if $(\frac{a}{p}) = 1$ (Unit square criterion and root count modulo odd prime powers).

[L2]

For powers of $2$ , the unit square criterion is automatic modulo $2$ , is $a \equiv 1 (m o d 4)$ modulo $4$ , and is $a \equiv 1 (m o d 8)$ modulo $2^{k}$ for $k \geq 3$ (Unit square criterion and root count modulo powers of two).

[L3]

For pairwise coprime positive integers $n_{i}$ with product $N$ , the Chinese remainder map gives $(Z / N)^{\times} ≅ \prod_{i} (Z / n_{i})^{\times}$ , including the empty list (For pairwise coprime positive moduli, the Chinese remainder bijection restricts to an isomorphism of unit groups).

[L4]

The prime factors and exponents in the canonical factorisation of a positive integer are determined by that integer (For $n \geq 1$ and any injective list $p : r \to Z$ of primes containing every prime divisor of $n$ , one has $n = \prod_{i < r} p_{i}^{v_{p_{i}} (n)}$ ; the exponents are determined by $n$ , and $v_{q} (n) = 0$ for every prime $q$ outside the list).

[L5]

Every positive integer has a finite prime factorisation, unique up to the order of its prime factors (The fundamental theorem of arithmetic: every integer $n \geq 1$ is a product of primes, and the factorisation is unique up to order — if $\prod_{i < r} p_{i} = \prod_{j < s} q_{j}$ with every $p_{i}$ and $q_{j}$ prime, then $r = s$ and $q_{i} = p_{π (i)}$ for some $π \in Sym (r)$ ).

Proof

technique · direct

1.1

By [L5], $n$ has a finite prime factorisation; grouping equal factors and using [L4] gives its uniquely determined nontrivial prime-power factors, which are pairwise coprime. Apply [L3] to identify the unit group modulo $n$ with the product of their unit groups; when $n = 1$ , this is the empty product of groups and has one element.

L3L4L5

2.1

Under the isomorphism of step 1.1, a global square maps to a square in every component. Conversely, if every component is a square, choose one root in each of the finitely many nonempty local root sets and apply the inverse CRT isomorphism to obtain a global root. Substitution of [L1] and [L2] gives the explicit local conditions in the Statement, and the empty product handles $n = 1$ .

step 1.1L1L2L3choose∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 114 results over 28 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

P. Hackman, Elementary Number Theory, §B.VII (standard reference, not scraped)
V. Shoup, A Computational Introduction to Number Theory and Algebra, 2nd ed., §12.4 (standard reference, not scraped)

A unit is a square modulo nn exactly when it is a square at every prime-power factor