Euler's criterion for the Legendre symbol defined by Gauss's count

Identifier: F:int-legendre-sym-modeq-pow
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For an odd prime `pp = 2m+1` and a natural `a` coprime to it, `a^m == legendreSym m a (mod pp)`, where `Int.legendreSym m a := (-1)^(gaussNegCount (2m+1) a m)`. THIS IS WHAT MAKES THE NAME HONEST. There was no Legendre symbol in this kernel (measured ABSENT against a declarations=2133 positive control). The classical definition is the residue indicator, and this kernel cannot prove that definition equals anything computable: `qr_criterion.rs` records that the CONVERSE of Euler's criterion needs a primitive root or a root-counting argument with no statable form here. So the symbol is defined by Gauss's counting exponent instead, and this theorem is the Euler-criterion characterization that pins it: a nonzero residue class mod an odd prime contains at most one of 1 and -1, so the congruence determines the symbol uniquely. HOW IT IS PROVED: it is `Int.gaussLemmaSignCount` read through the definition -- the two conclusions differ only by delta, so the proof is the application itself, and a test asserts `def_eq` of the two declared types while also asserting their RENDERED TEXT differs (which is the point of having the definition). WHAT IS NOT PROVED: `legendreSym m a = 1 <-> Int.is_quadratic_residue (ofNat pp) (ofNat a)`, in either direction. `Kernel::axiom_footprint` is EMPTY. Admitted on the first attempt.

Formal statement

theorem Int.legendreSym_modEq_pow : ((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.legendreSym x0 x1)))))

Dependencies

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

1 direct dependencies 0 direct dependents

Evidence

kernel-Int.legendreSym_modEq_pow

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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.legendreSym_modEq_pow

Kind: exhaustive-enumeration
Status: checked

Supports: ADR-1557's check script verifies a^m mod pp equals the sign (-1)^gaussNegCount reduced mod pp at every odd prime and coprime multiplier it sweeps, including multipliers whose counts have opposite parity.

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)."
}