Reciprocity law · Native PA

Quadratic Reciprocity

(p/q)(q/p) = (−1)((p−1)(q−1))/4

A complete 557-theorem reading surface, from the Peano axioms through Gauss and Eisenstein counting arguments to the final reciprocity theorem.

Open the definition-aware map Read the final theorem Locate it in the grand campaign

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.

Exact certificate

Fully expanded PA

Inspect the native first-order statements, all 27,491 tactic lines, and the complete 1,787-edge dependency graph.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem PA00FW and display only the definitions and lemmas that support the capstone.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → reciprocity family → proved quadratic reciprocity → theorem and definition dependencies. Future milestones include Jacobi reciprocity, cubic reciprocity, and quartic reciprocity; these remain open.
Frozen artifact: 557 theorems · 1,787 proof edges · 40 definitions · 45 layers.