The full sum-of-two-squares characterisation for composite n (OPEN, and deliberately out of scope for the lane that opened it)

Identifier: F:int-two-squares-composite-characterisation
Proof route: Not assigned
External status: proved
Axiom footprint: Empty

Recorded description

A positive integer n is a sum of two integer squares if and only if every prime congruent to 3 modulo 4 occurs to an EVEN exponent in the prime factorisation of n. NOT ESTABLISHED HERE and deliberately not attempted. The forward direction needs Fermat's theorem for the primes congruent to 1 modulo 4 (F:int-fermat-two-squares, itself open) together with the multiplicativity that IS proved (F:int-sum-of-two-squares-multiplicative); the reverse direction needs the mod-4 refutation lifted from n itself to each prime power, which needs unique factorisation as a MULTISET and not merely the existence of a factorisation.

Formal statement

forall (n : Nat), 0 < n -> (Int.IsSumOfTwoSquares (Int.ofNat n) <-> forall (q : Nat), Nat.IsPrime q -> Nat.ModEq 4 q 3 -> Nat.Even (Nat.factorization n q))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

3 direct dependencies 0 direct dependents

Evidence

Provenance

{
  "date": "2026-09-05",
  "curation": "curated",
  "established_by": "not established in this ledger",
  "source": "the classical sum-of-two-squares theorem for general n (Euler, Gauss); registered by the two-squares lane (W3-10, ADR-1633) as the explicitly out-of-scope continuation of the graded family",
  "prior_art": [
    {
      "who": "Fermat; Euler; Gauss",
      "what": "the characterisation of the integers representable as a sum of two squares",
      "year": 1801,
      "where": "Disquisitiones Arithmeticae and earlier correspondence",
      "attribution": "standard textbook attribution; this lane did not consult the primary sources"
    }
  ]
}