Gauss's lemma (quadratic residues), over the constructed integers

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

Recorded description

Gauss's lemma, the sign-counting criterion: for an odd modulus pp = 2m+1 satisfying this kernel's PrimeCond and a multiplier a coprime to pp, a^m is congruent to (-1)^N modulo pp, where N = gaussNegCount pp a m is the number of k in 1..m whose least positive residue of a*k mod pp exceeds pp/2. Nothing here is imported or axiomatised: the count is this kernel's own `AxNat.countRange (fun j => AxNat.gaussSignNeg pp a (succ j)) m`, built from `AxNat.mod`/`AxNat.ble`, and the congruence is `Int.ModEq`, which unfolds to an `Int.emod` equality over the constructed integers. `Kernel::axiom_footprint` for this declaration is EMPTY. WHAT THIS DOES NOT CLAIM. It is the connecting theorem, not the quadratic-reciprocity supplement that consumes it: no evaluation of gaussNegCount at a general a is asserted (only the a := 2 closed form `Nat.gaussNegCountTwoClosedForm` exists, separately), so the mod-8 criterion for whether 2 is a quadratic residue is NOT established here. Both hypotheses are load-bearing and neither is discharged: primality is what makes m! invertible mod pp, and coprimality of a is what makes the signed-fold map injective. The oddness of the modulus is structural rather than hypothetical -- pp is written `succ (mul 2 m)`, so no even modulus can be substituted. Note the name: `Int.gauss_lemma` in this same prelude is EUCLID's lemma, a different theorem carrying the same common misnomer.

Formal statement

theorem Int.gaussLemmaSignCount : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : And (AxNat.le (AxNat.succ (AxNat.succ AxNat.zero)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (((x2 : AxNat) -> ((x3 : AxNat.dvd x2 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) -> Or (Eq.{1} AxNat x2 (AxNat.succ AxNat.zero)) (Eq.{1} AxNat x2 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))))))) -> ((x3 : Eq.{1} AxNat (AxNat.gcd x1 (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (AxNat.succ AxNat.zero)) -> Int.ModEq (Int.ofNat (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0))) (Int.pow (Int.ofNat x1) x0) (Int.pow (Int.neg Int.one) (AxNat.gaussNegCount (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)) x1 x0))))))

Dependencies

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

17 direct dependencies 2 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Int.gaussLemmaSignCount

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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.gaussLemmaSignCount. 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": "curated",
  "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 gauss-final, ADR-1130); every other field is the generator's output unmodified."
}