The second supplementary law of quadratic reciprocity, over the constructed integers

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

Recorded description

The second supplementary law of quadratic reciprocity, in its Legendre-symbol (power-residue) form. For an odd modulus p = 2m+1 satisfying this kernel's PrimeCond, 2^m is congruent to +1 modulo p exactly when p is congruent to 1 or 7 modulo 8, and to -1 exactly when p is congruent to 3 or 5 modulo 8. The residue class is stated structurally rather than through a `mod 8` term: with q := div (div m 2) 2, the theorem's disjunction names m = 4q, 4q+1, 4q+2, 4q+3 (equivalently p = 8q+1, 8q+3, 8q+5, 8q+7) as the four shapes, and because those four are exhaustive and pairwise distinct the single disjunction gives BOTH directions of each line. Nothing here is imported or axiomatised: the modulus, the power and the count are this kernel's own constructions, the congruence is `Int.ModEq` over the constructed integers, and `Kernel::axiom_footprint` for this declaration is EMPTY. WHAT THIS DOES NOT CLAIM. It is the POWER-RESIDUE form, not the classical `IsQuadraticResidue` form. Half of that classical statement follows and is a separate proposition -- Euler's criterion's -1 detector (`Int.euler_criterion_neg_one_imp_not_residue`) turns the `= -1` line into `2 is NOT a quadratic residue mod p` for p congruent to 3 or 5 mod 8. The other half (p congruent to +-1 mod 8 implies 2 IS a residue) needs the CONVERSE of Euler's criterion, 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. Primality is load-bearing and is not discharged: it is what Gauss's lemma needs to make m! invertible mod p. Coprimality of the multiplier is NOT a hypothesis -- p = succ (mul 2 m) is odd by construction, so gcd 2 p = 1 is derived in-proof from `Nat.coprime_two_left`.

Formal statement

theorem Int.secondSupplementaryLaw : ((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))))))) -> Or (And (Or (Eq.{1} AxNat x0 (AxNat.add (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero)))) (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero)))))) (Eq.{1} AxNat x0 (AxNat.succ (AxNat.add (AxNat.succ (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))))) (AxNat.succ (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))))))))) (Int.ModEq (Int.ofNat (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (Int.pow (Int.ofNat (AxNat.succ (AxNat.succ AxNat.zero))) x0) Int.one)) (And (Or (Eq.{1} AxNat x0 (AxNat.succ (AxNat.add (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero)))) (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))))))) (Eq.{1} AxNat x0 (AxNat.add (AxNat.succ (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))))) (AxNat.succ (AxNat.add (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.div (AxNat.div x0 (AxNat.succ (AxNat.succ AxNat.zero))) (AxNat.succ (AxNat.succ AxNat.zero)))))))) (Int.ModEq (Int.ofNat (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (Int.pow (Int.ofNat (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.

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

Evidence

kernel-Int.secondSupplementaryLaw

Kind: kernel-term
Status: checked

Supports: Int.secondSupplementaryLaw 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.secondSupplementaryLaw 2>/dev/null | grep -cE '^Int\.secondSupplementaryLaw[[: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.secondSupplementaryLaw

Kind: exhaustive-enumeration
Status: checked

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

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.secondSupplementaryLaw. 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 second-supplementary-law, ADR-1150); every other field is the generator's output unmodified."
}