ExampleConstruction: AI-generatedVerification: AI-generatedSession-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 complete reciprocity table for $3, 5, 7, 11$

Example

The nonzero square classes for the primes $3, 5, 7, 11$ are

$p$	nonzero squares modulo $p$
$3$	$1$
$5$	$1, 4$
$7$	$1, 2, 4$
$11$	$1, 3, 4, 5, 9$

Using the definition of the Legendre symbol (The Legendre symbol, including its zero value) gives the complete pair table

${p, q}$	$(p / q)$	$(q / p)$	relation
${3, 5}$	$- 1$	$- 1$	agree
${3, 7}$	$- 1$	$1$	opposite
${3, 11}$	$1$	$- 1$	opposite
${5, 7}$	$- 1$	$- 1$	agree
${5, 11}$	$1$	$1$	agree
${7, 11}$	$- 1$	$1$	opposite

The signs are opposite exactly when both primes are congruent to $3$ modulo $4$ , as predicted by quadratic reciprocity (Quadratic reciprocity for distinct odd primes).

Facts & Assumptions

Given: The primes $3, 5, 7, 11$ and the residue tables displayed in the Example.

[L1]

For distinct odd primes $p, q$ , $(\frac{p}{q}) (\frac{q}{p}) = (- 1)^{(p - 1) (q - 1) / 4}$ (Quadratic reciprocity for distinct odd primes).

[L2]

For an odd prime $p$ , the Legendre symbol is $1$ on nonzero square classes, $- 1$ on nonzero nonsquare classes, and $0$ on the zero class (The Legendre symbol, including its zero value).

Verification

technique · direct

1.1

Squaring every residue class modulo each prime gives the displayed nonzero square sets. Reading the residues of each numerator from those sets by [L2] gives all entries in the pair table.

L2givenalgebra

2.1

For the pairs ${3, 7}$ , ${3, 11}$ , and ${7, 11}$ both primes are $3$ modulo $4$ and the direct signs are opposite; in every other row at least one prime is $1$ modulo $4$ and the signs agree. Each row therefore has the product required by [L1].

step 1.1L1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

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

A complete reciprocity table for 3,5,7,113,5,7,11