The first supplementary law of quadratic reciprocity, non-residue half, over the constructed integers

Identifier: F:int-firstsupplementarylawnotresidue
Proof route: kernel-lean
External status: Not recorded
Axiom footprint: Empty

Recorded description

The non-residue half of the first supplementary law of quadratic reciprocity. For a modulus p = 2m+1 satisfying this kernel's PrimeCond, with m ODD -- equivalently p congruent to 3 modulo 4 -- the integer -1 is NOT a quadratic residue modulo p, where `Int.IsQuadraticResidue p a` is this prelude's own definition, the existence of an x with x*x congruent to a modulo p. Nothing here is imported or axiomatised: the modulus is this kernel's constructed natural, the congruence is `Int.ModEq` over the constructed integers, and `Kernel::axiom_footprint` for this declaration is EMPTY. WHAT THIS DOES NOT CLAIM. The full law is a biconditional -- -1 is a residue mod p exactly when p is congruent to 1 modulo 4 -- and only the non-residue direction is proved here. The other direction needs a WITNESS, and the Euler-criterion route to one requires the CONVERSE of Euler's criterion (a^((p-1)/2) congruent to 1 implies a is a residue), which needs a primitive root or a root-counting argument over a polynomial ring this kernel has no List/Finset to state; `int_prelude/qr_criterion.rs`'s module doc records that gap and this theorem does not close it. So do not read this fact as deciding -1's residue-hood; it decides it in one direction only. Primality is load-bearing and is not discharged: it is what Euler's criterion needs. `Nat.Odd m` is load-bearing too and the theorem is FALSE without it -- at even m the conclusion is the opposite one (mod 5, -1 is a residue, witness 2).

Formal statement

theorem Int.firstSupplementaryLawNotResidue : ((x0 : AxNat) -> ((x1 : And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (((x1 : AxNat) -> ((x2 : AxNat.dvd x1 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) -> Or (Eq.{1} AxNat x1 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x1 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))))))) -> ((x2 : AxNat.Odd x0) -> Not (Int.is_quadratic_residue (Int.ofNat (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (Int.neg Int.one)))))

Dependencies

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

23 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.firstSupplementaryLawNotResidue

Kind: kernel-term
Status: checked

Supports: Int.firstSupplementaryLawNotResidue 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.firstSupplementaryLawNotResidue 2>/dev/null | grep -cE '^Int\.firstSupplementaryLawNotResidue[[: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. 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: this tool builds creal/complex/cpoint, which overflow the default debug thread stack.

footprint-Int.firstSupplementaryLawNotResidue

Kind: exhaustive-enumeration
Status: checked

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

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 integer surface bounds every declaration in it, including Int.firstSupplementaryLawNotResidue. This is a whole-prelude bound, not a per-declaration measurement; the per-declaration figure is the footprint column of kernel_declaration_projection, measured 0 for this row.

Provenance

{
  "date": "2026-08-31",
  "curation": "generated-unreviewed",
  "generated_by": "scripts/gen-kernel-facts.py",
  "established_by": "axeyum-lean-kernel build_int_prelude (crates/axeyum-lean-kernel/src/int_prelude/)",
  "source": "Derived mechanically from the unfiltered emit of `cargo run -q --release -p axeyum-lean-kernel --example kernel_declaration_projection`, which prints one TSV row per declaration whose fields are (prelude, kind, display name, axiom-footprint size, direct type declarations, direct declarations, direct theorems, Kernel::render_lean(declaration.ty())). formal.statement is that last field verbatim; depends_on is the direct-theorem column intersected with this ledger's registered facts; axiom_footprint is the footprint-size column, cross-checked by the whole-prelude nat_axiom_inventory run recorded in the second evidence row. No field was hand-transcribed and no prose was authored. `title`, `statement` and `notes` were then REPLACED by hand (lane first-supplementary-law, ADR-1230); every other field is the generator's output unmodified."
}