Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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≥1 and let [a]n∈(Z/n)×. 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 2e, there is no additional condition when e≤1, one needs a≡1(mod4) when e=2, and one needs a≡1(mod8) when e≥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≥1, and p∤a, the congruence x2≡a(modpk) is soluble if and only if (ap)=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≡1(mod4) modulo 4, and is a≡1(mod8) modulo 2k for k≥3 (Unit square criterion and root count modulo powers of two).

[L3]

For pairwise coprime positive integers ni with product N, the Chinese remainder map gives (Z/N)×≅∏i(Z/ni)×, including the empty list (For pairwise coprime positive moduli, the Chinese remainder bijection restricts to an isomorphism of unit groups).

Proof

technique · direct
1.1L3L4L5

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.

2.1step 1.1L1L2L3choose∎

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.

Depends on

Used by

Dependency tree · two levels

46 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