The two Gauss counting exponents sum to n*m modulo 2

Identifier: F:nat-gausscount-sum-modeq
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

The congruence form of `Nat.gaussCount_sum_even`: for odd `pp = 2m+1` and odd `q = 2n+1` with `gcd q pp = 1`, `Nat.modEq 2 (gaussNegCount pp q m + gaussNegCount q pp n) (n*m)`. `Nat.modEq d a b := exists u v, a + d*u = b + d*v` is the BALANCED form (`modular.rs`), which is what makes this a corollary at `u := n*m`, `v := k` rather than a second proof: from `S + T = k + k` one has `S + 2*T = (S + T) + T = (k + k) + T` and `T + 2*k = T + (k + k)`, which differ by one `add_comm`. The same route `Nat.eisenstein_lemma_modEq` takes from `Nat.eisenstein_lemma`. `Kernel::axiom_footprint` is EMPTY. Admitted on the first attempt.

Formal statement

theorem Nat.gaussCount_sum_modEq : ((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)) -> AxNat.modEq (AxNat.succ (AxNat.succ AxNat.zero)) (AxNat.add (AxNat.gaussNegCount (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1)) x0) (AxNat.gaussNegCount (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x1)) (AxNat.succ (AxNat.mul (AxNat.succ (AxNat.succ AxNat.zero)) x0)) x1)) (AxNat.mul x1 x0))))

Dependencies

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

7 direct dependencies 0 direct dependents

Evidence

kernel-Nat.gaussCount_sum_modEq

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the nat prelude's trusted surface is empty, which bounds Nat.gaussCount_sum_modEq.

Checker command

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

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-Nat.gaussCount_sum_modEq

Kind: exhaustive-enumeration
Status: checked

Supports: ADR-1557's check script verifies the congruence's two sides agree modulo 2 at every pair it sweeps, and that the witnesses u := n*m, v := k really satisfy the balanced equation.

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_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/quadratic_reciprocity_count.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)."
}