The least residues reconcile with the folded ones

Identifier: F:nat-leastresidue-sumrange-reconcile
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every modulus `pp = succ ap`, every multiplier `a` and every bound `m`: `SUM leastResidue + 2 * SUM_{sign} gaussFold = SUM gaussFold + pp * gaussNegCount`. This is ADR-1540's and ADR-1544's RESIDUE 2, the reconciliation both lanes named and neither could state. TWO DELIBERATE RESTATEMENTS. (1) ADDITIVE, not subtractive: both prior lanes wrote it as `SUM leastResidue = SUM gaussFold + pp*N - 2*SUM_neg gaussFold`, which cannot be stated here as written because `Nat.sub` is TRUNCATED and nothing in that statement bounds the subtrahend. Moving the negative term across makes it unambiguous over the naturals and identical over the integers. (2) `x + x`, not `2 * x`: `Nat.mul` recurses on its RIGHT argument, so `mul 2 SUM` is stuck at a symbolic sum and would need a `two_mul` bridge this prelude does not have. IT HAS NO HYPOTHESIS, AND THAT IS THE FINDING: coprimality is what makes the FOLD a bijection (`Nat.gauss_fold_sumRange_eq`), not what makes a residue and its reflection add to `pp`. The only side condition the argument needs is `leastResidue < pp`, which `Nat.mod_lt` supplies at the constructively positive modulus `succ ap`. So the earlier handoffs were wrong in one direction: residue 2 was never blocked on Gauss's lemma or on coprimality, only on `Nat.sumRangeIf`, which did not exist. HOW IT IS PROVED: one pointwise `Bool.rec` on the sign -- whose motive has to abstract the sign TWICE, because `gaussFold` contains it by delta and has no variable to abstract -- lifted by `Nat.sumRange_congr`, three `Nat.sumRange_add`s, `Nat.mul_sumRange` and `Nat.countRange_eq_sumRange`, whose result IS `gaussNegCount` by delta with no bridging step. `Kernel::axiom_footprint` is EMPTY. Admitted on the first attempt.

Formal statement

theorem Nat.leastResidue_sumRange_reconcile : ((x0 : AxNat) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.add (AxNat.sumRange (fun (x3 : AxNat) => AxNat.leastResidue (AxNat.succ x0) x1 (AxNat.succ x3)) x2) (AxNat.add (AxNat.sumRangeIf (fun (x3 : AxNat) => AxNat.gaussSignNeg (AxNat.succ x0) x1 (AxNat.succ x3)) (fun (x3 : AxNat) => AxNat.gaussFold (AxNat.succ x0) x1 (AxNat.succ x3)) x2) (AxNat.sumRangeIf (fun (x3 : AxNat) => AxNat.gaussSignNeg (AxNat.succ x0) x1 (AxNat.succ x3)) (fun (x3 : AxNat) => AxNat.gaussFold (AxNat.succ x0) x1 (AxNat.succ x3)) x2))) (AxNat.add (AxNat.sumRange (fun (x3 : AxNat) => AxNat.gaussFold (AxNat.succ x0) x1 (AxNat.succ x3)) x2) (AxNat.mul (AxNat.succ x0) (AxNat.gaussNegCount (AxNat.succ x0) x1 x2))))))

Dependencies

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

13 direct dependencies 1 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.leastResidue_sumRange_reconcile

Kind: kernel-term
Status: checked

Supports: Nat.leastResidue_sumRange_reconcile 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.leastResidue_sumRange_reconcile 2>/dev/null | grep -cE '^Nat\.leastResidue_sumRange_reconcile[[: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. Pass ONE name per invocation: this tool silently keeps only the FIRST name argument.

footprint-Nat.leastResidue_sumRange_reconcile

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the natural-number prelude's trusted surface is empty, which bounds Nat.leastResidue_sumRange_reconcile.

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 nat 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 gauss_residue_reconcile_tests.rs.

numeric-Nat.leastResidue_sumRange_reconcile

Kind: exhaustive-enumeration
Status: checked

Supports: ADR-1552's check script sweeps this statement's arithmetic over 8450 (modulus, multiplier, bound) instances for the hypothesis-free rows, 519 coprime instances for the counting identity, and 399 coprime odd pairs plus all 240 ordered pairs of distinct odd primes below 60 for Eisenstein's lemma; the control table refutes eight wrong readings at named witnesses.

Checker command

python3 docs/research/09-decisions/adr-1552-eisenstein-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): 16 of 16 mutations exit 1. Two recorded SURVIVORS, M9 and M10, are the argument order of the congruence and of `Even (F + N)` -- invisible to every numeric check and guarded only by the character-for-character type pins in gauss_residue_reconcile_tests.rs.

Provenance

{
  "date": "2026-09-02",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/gauss_residue_reconcile.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 gauss_residue_reconcile_tests.rs). 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 -- direct dependencies with no fact row are omitted. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane eisenstein-3)."
}