Residues of −1 and 2 · Constructive arithmetic

Quadratic Supplementary Laws

(−1|p) = (−1)^((p−1)/2) · (2|p) = (−1)^((p²−1)/8)

Follow the complete constructive modulo-four and modulo-eight residue classifications.

Open the definition-aware map Read the final theorem See campaign milestone G044

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Recommended

Defined mathematical notation

Browse 23 linked conservative definitions and 30 theorem bodies without losing their exact first-order expansions.

Browse definitions and theorems →

Focused route

Complete dependency graph

Follow the selected theorem through its constructive prerequisites, linked definitions, and original proof scripts.

Trace prerequisites →

Exact certificate

Fully expanded arithmetic

Inspect 1382 original tactic lines and 100 dependency edges with every definition fully expanded.

Open the exact edition →
Independently verified Alpha v34 checked-use theorem family: 28 displayed closed proofs among 4223 checked release theorems; not Stable: 30 theorem bodies · 23 linked definitions · 17 definition-dependency arrows · 100 proof edges · 1382 tactic lines. dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged.