ExampleConstruction: AI-generatedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-26

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.

Descending from $13 \cdot 11$ to $13$ in two steps

Example

Start from the prime $p = 13$ and the multiplier $m = 11$ , with

$143 = 13 \cdot 11 = 11^{2} + 3^{2} + 3^{2} + 2^{2} .$

Centring the coordinates modulo $11$ gives $(0, 3, 3, 2)$ , whose norm is $22 = 11 \cdot 2$ , so the multiplier drops to $n = 2$ . Euler's identity applied to $(11, 3, 3, 2)$ and $(0, 3, 3, 2)$ gives $(22, 33, 33, 22)$ , each coordinate divisible by $11$ ; dividing by $11$ gives

$26 = 13 \cdot 2 = 2^{2} + 3^{2} + 3^{2} + 2^{2} .$

Repeating with $m = 2$ : the centred quadruple is $(0, 1, 1, 0)$ , of norm $2 = 2 \cdot 1$ , so $n = 1$ ; the identity applied to $(2, 3, 3, 2)$ and $(0, 1, 1, 0)$ gives $(6, 4, 0, 0)$ , and dividing by $2$ gives

$13 = 3^{2} + 2^{2} + 0^{2} + 0^{2} .$

The two steps use an odd modulus and then an even one, so both parities occur.

Facts & Assumptions

Given: The prime $13$ , the multiplier $11$ , and the representation $143 = 11^{2} + 3^{2} + 3^{2} + 2^{2}$ .

[F1]

A representation of a nonnegative integer $n$ as a sum of four squares is an ordered quadruple $(a, b, c, d) \in Z^{4}$ with $n = a^{2} + b^{2} + c^{2} + d^{2}$ (Representations as sums of four squares).

[L1]

If $p$ is prime, $1 < m < p$ and $p m$ is a sum of four integer squares, then there is an integer $n$ with $1 \leq n < m$ for which $p n$ is a sum of four integer squares (Descent step: a smaller multiple of $p$ is a sum of four squares).

[L2]

If $p$ is prime, $1 < m < p$ and $p m = a^{2} + b^{2} + c^{2} + d^{2}$ , then the least absolute remainders $a^{'}, b^{'}, c^{'}, d^{'}$ of $a, b, c, d$ modulo $m$ satisfy $a^{' 2} + b^{' 2} + c^{' 2} + d^{' 2} = m n$ for an integer $n$ with $1 \leq n < m$ (The centred residue quadruple of $p m = a^{2} + b^{2} + c^{2} + d^{2}$ has norm $m n$ with $1 \leq n < m$ ).

[L3]

For an integer $m \geq 1$ and $a \in Z$ there is exactly one integer $r$ with $a \equiv r (m o d m)$ and $- m < 2 r \leq m$ , and consequently $4 r^{2} \leq m^{2}$ (The least absolute remainder modulo a positive integer).

[L4]

For all integers $x_{1}, \dots, x_{4}, y_{1}, \dots, y_{4}$ , setting $z_{1} = x_{1} y_{1} + x_{2} y_{2} + x_{3} y_{3} + x_{4} y_{4}$ , $z_{2} = x_{1} y_{2} - x_{2} y_{1} - x_{3} y_{4} + x_{4} y_{3}$ , $z_{3} = x_{1} y_{3} + x_{2} y_{4} - x_{3} y_{1} - x_{4} y_{2}$ and $z_{4} = x_{1} y_{4} - x_{2} y_{3} + x_{3} y_{2} - x_{4} y_{1}$ gives $(x_{1}^{2} + x_{2}^{2} + x_{3}^{2} + x_{4}^{2}) (y_{1}^{2} + y_{2}^{2} + y_{3}^{2} + y_{4}^{2}) = z_{1}^{2} + z_{2}^{2} + z_{3}^{2} + z_{4}^{2}$ (Euler's four-square product identity).

Verification

technique · direct

1.1

The starting datum is a representation: $11^{2} + 3^{2} + 3^{2} + 2^{2} = 121 + 9 + 9 + 4 = 143$ and $13 \cdot 11 = 143$ , with $1 < 11 < 13$ as [L1] and [L2] require.

givenF1algebra

2.1

By [L3] with modulus $11$ , the least absolute remainders of $11, 3, 3, 2$ are $0, 3, 3, 2$ , since $11 - 0 = 11$ is a multiple of $11$ and $- 11 < 2 r \leq 11$ holds for $r = 0, 3, 2$ ; their norm is $0 + 9 + 9 + 4 = 22 = 11 \cdot 2$ , so the integer $n$ of [L2] is $2$ , and indeed $1 \leq 2 < 11$ .

step 1.1L2L3algebra

3.1

Applying [L4] to $x = (11, 3, 3, 2)$ and $y = (0, 3, 3, 2)$ gives $z_{1} = 11 \cdot 0 + 3 \cdot 3 + 3 \cdot 3 + 2 \cdot 2 = 22$ , $z_{2} = 11 \cdot 3 - 3 \cdot 0 - 3 \cdot 2 + 2 \cdot 3 = 33$ , $z_{3} = 11 \cdot 3 + 3 \cdot 2 - 3 \cdot 0 - 2 \cdot 3 = 33$ and $z_{4} = 11 \cdot 2 - 3 \cdot 3 + 3 \cdot 3 - 2 \cdot 0 = 22$ , whose squares sum to $484 + 1089 + 1089 + 484 = 3146 = 143 \cdot 22$ ; each coordinate is divisible by $11$ , and dividing gives $(2, 3, 3, 2)$ with $4 + 9 + 9 + 4 = 26 = 13 \cdot 2$ , which is the conclusion of [L1] at $n = 2$ .

step 2.1L1L4algebra

4.1

Repeating with $p = 13$ and $m = 2$ , for which $1 < 2 < 13$ : by [L3] with modulus $2$ the least absolute remainders of $2, 3, 3, 2$ are $0, 1, 1, 0$ , since $2 r = 2$ is admitted for $r = 1$ ; their norm is $0 + 1 + 1 + 0 = 2 = 2 \cdot 1$ , so [L2] gives $n = 1$ with $1 \leq 1 < 2$ .

step 3.1L2L3algebra

5.1

Applying [L4] to $x = (2, 3, 3, 2)$ and $y = (0, 1, 1, 0)$ gives $z_{1} = 2 \cdot 0 + 3 \cdot 1 + 3 \cdot 1 + 2 \cdot 0 = 6$ , $z_{2} = 2 \cdot 1 - 3 \cdot 0 - 3 \cdot 0 + 2 \cdot 1 = 4$ , $z_{3} = 2 \cdot 1 + 3 \cdot 0 - 3 \cdot 0 - 2 \cdot 1 = 0$ and $z_{4} = 2 \cdot 0 - 3 \cdot 1 + 3 \cdot 1 - 2 \cdot 0 = 0$ , whose squares sum to $36 + 16 = 52 = 26 \cdot 2$ ; each coordinate is divisible by $2$ , and dividing gives $(3, 2, 0, 0)$ with $9 + 4 = 13$ , a representation of $13$ itself.

step 4.1L1L4algebra

6.1

So two applications of the descent carry $13 \cdot 11$ to $13 \cdot 2$ and then to $13 \cdot 1$ , the moduli used being $11$ and $2$ .

step 3.1step 5.1F1∎

Remarks

The even step is where the tie could have bitten. At $m = 2$ the centred coordinates $1$ attain $2 r = m$ , so the estimate $4 r^{2} \leq m^{2}$ is an equality in two of the four coordinates. That is admissible: what The centred residue quadruple of $p m = a^{2} + b^{2} + c^{2} + d^{2}$ has norm $m n$ with $1 \leq n < m$ excludes is equality in all four at once, and here two coordinates centre to $0$ .

The starting representation is not the minimal one. The descent does not require the multiplier to come from Some multiple $p m$ with $1 \leq m < p$ is a sum of four squares; any $m$ with $1 < m < p$ for which $p m$ is a sum of four squares will do, and $m = 11$ was taken to make two steps rather than one.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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

Keith Conrad, Proofs by Descent, §6, Theorem 6.6 (standard reference, not scraped)

Descending from 13⋅1113⋅11 to 1313 in two steps