The law of quadratic reciprocity

Identifier: F:int-quadratic-reciprocity
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

THE LAW OF QUADRATIC RECIPROCITY. For odd `pp = 2m+1` and odd `q = 2n+1` with `gcd q pp = 1`, `legendreSym m q * legendreSym n pp = (-1)^(n*m)`. At two distinct odd primes `p` and `q` with `m = (p-1)/2`, `n = (q-1)/2` this is the classical `(q|p)(p|q) = (-1)^((p-1)/2 * (q-1)/2)`, i.e. the two symbols differ exactly when both primes are 3 mod 4. HOW IT IS PROVED: all the mathematics is on the Nat side, in `Nat.gaussCount_sum_even`, which is itself the assembly of Eisenstein's lemma at (m,n) and (n,m) with the min-free floor-sum identity. What remains is ring algebra. Writing `A := (-1)^N_p`, `B := (-1)^N_q`, `C := (-1)^(n*m)`, `S := N_p + N_q` and `T := n*m`: `Int.pow_add` gives `(A*B)*C = (-1)^(S+T)`, which `Int.pow_neg_one_of_even` turns into 1 using `Even (S+T)`; the same two steps give `C*C = (-1)^(T+T) = 1` with witness `k := T`; and then `A*B = (A*B)*1 = (A*B)*(C*C) = ((A*B)*C)*C = 1*C = C`. MULTIPLYING BY THE SELF-INVERSE C DELIBERATELY AVOIDS A PARITY CASE SPLIT: the obvious route -- case on Even S / Odd S and transfer the parity to T -- needs two `Even (a+b) -> ...` transfer lemmas this prelude does not have. WHAT IS ASSUMED: only coprimality of the two odd numbers, NEVER primality, so this statement is strictly stronger than the textbook law. Primality is needed only for the symbol's Euler-criterion specification (`Int.legendreSym_modEq_pow`), where Gauss's lemma uses it to cancel m!. COPRIMALITY IS LOAD-BEARING: at `pp = q = 3` the left side reduces to +1 and the right to -1, refuted inside the kernel. `Kernel::axiom_footprint` is EMPTY. Admitted on the first attempt.

Formal statement

theorem Int.quadraticReciprocity : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : Eq.{1} AxNat (AxNat.gcd (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (AxNat.succ AxNat.zero)) -> Eq.{1} Int (Int.mul (Int.legendreSym x0 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1))) (Int.legendreSym x1 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)))) (Int.pow (Int.neg Int.one) (AxNat.mul x1 x0)))))

Dependencies

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

6 direct dependencies 0 direct dependents

Evidence

kernel-Int.quadraticReciprocity

Kind: kernel-term
Status: checked

Supports: Int.quadraticReciprocity is admitted by the trusted kernel gate with the type recorded in formal.statement.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example theorem_dependency_inventory -- Int.quadraticReciprocity 2>/dev/null | grep -cE '^Int\.quadraticReciprocity[[:space:]]'

Evidence notes

Two independent failure modes, so the exit status depends on the finding rather than on the run completing: theorem_dependency_inventory exits non-zero when a NAMED filter matches nothing, and grep -c exits 1 printing 0 when the anchored line is absent. RUN WITH A NEGATIVE CONTROL and it was: the real name prints 1 with both pipeline stages at 0, a one-character typo prints 0 with both stages at 1. Anchored with [[:space:]], never \t -- in a scripted (GNU) grep \t is a literal t. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. --release is MANDATORY (the debug build SIGABRTs). Pass ONE name per invocation: this tool silently keeps only the FIRST name argument, and a PREBUILT copy reports a just-declared theorem ABSENT (ADR-1552 finding 5), which is why the command runs `cargo run` rather than the binary.

footprint-Int.quadraticReciprocity

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the integer prelude's trusted surface is empty, which bounds Int.quadraticReciprocity.

Checker command

cargo run -q --release -p axeyum-lean-kernel --example nat_axiom_inventory -- --require-axiom-free integer

Evidence notes

--require-axiom-free exits non-zero when the named prelude's trusted surface (Axiom + Opaque + Quotient) is not empty, and errors rather than silently passing for a prelude the run never built. A declaration cannot depend on a trusted declaration the environment does not contain, so an empty surface bounds every declaration in it. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is measured 0 by the axiom-footprint assertion in the module's test file.

numeric-Int.quadraticReciprocity

Kind: exhaustive-enumeration
Status: checked

Supports: ADR-1557's check script re-derives both Legendre symbols from gaussNegCount's own definition and verifies the law at every coprime odd pair below a bound and at all ordered pairs of distinct odd primes below 60, together with the non-coprime refutation and its recorded survivor.

Checker command

python3 docs/research/09-decisions/adr-1557-quadratic-reciprocity-checks.py

Evidence notes

Exit status depends on the finding: a claim that fails, or a control that behaves other than as recorded, exits 1. Verified by mutating the script itself in a scratch copy with one uniquely-named file per mutant (so the stale-__pycache__ trap cannot report the previous mutant's result).

Provenance

{
  "date": "2026-09-02",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/quadratic_reciprocity.rs)",
  "source": "formal.statement is taken verbatim from the kernel's own rendering (Kernel::render_lean of the admitted declaration type; the same string is pinned character for character in the module's test file). depends_on is the direct-theorem column of theorem_dependency_inventory intersected with this ledger's registered facts, so it is an INTERSECTION and not the full dependency set -- Nat.gcd_comm is a direct dependency of Nat.gaussCount_sum_even with no fact row and is therefore omitted. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane quadratic-reciprocity-2)."
}