Summing over a range is invariant under an injective self-map

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

Recorded description

For an injective self-map `sigma` of `[0,n)`, `sumRange f n = sumRange (f . sigma) n`. WHY IT IS THE POINT: Gauss's lemma already runs this bijection MULTIPLICATIVELY -- `Int.prodRange_permute` at the self-map induced by `Nat.gaussFold` is what turns the product of folded least residues into `m!` (`int_prelude/gauss_assembly.rs`). Eisenstein's lemma needs the same bijection ADDITIVELY, to turn the SUM of folded least residues into the sum over `[1,m]`, and no aggregate in this kernel had a `Nat`-valued permutation law. HOW IT IS PROVED: induction on `n` with `f` quantified outside and the motive generalized over `sigma` (generalizing over `f` instead does not close -- the recursive call reuses `f` and only `sigma` moves). At `succ n` the pigeonhole `Nat.injective_on_imp_surjective_on` locates `i0 < succ n` with `sigma i0 = n`; when `i0 = n` the map already fixes the top index and the hypotheses restrict by pure bound-weakening, and when `i0 < n` the argument restricts along the single-point override `Nat.restrict_injective` / `Nat.restrict_maps_into` and closes with `Nat.sumRange_point_change`. IT IS NOT A COROLLARY of `Nat.countRange_permute`, and the direction matters: `countRange_eq_sumRange` is `Eq.refl`, so counting IS summing a `{0,1}`-valued family, which makes the counting theorem the special case of this one rather than the reverse. `Kernel::axiom_footprint` is EMPTY. Admitted by the trusted gate on the first attempt.

Formal statement

theorem Nat.sumRange_permute : ((x0 : ((x0 : AxNat) -> AxNat)) -> ((x1 : ((x1 : AxNat) -> AxNat)) -> ((x2 : AxNat) -> ((x3 : AxNat.injectiveOn x1 x2) -> ((x4 : AxNat.mapsInto x1 x2) -> Eq.{1} AxNat (AxNat.sumRange x0 x2) (AxNat.sumRange (fun (x5 : AxNat) => x0 (x1 x5)) x2))))))

Dependencies

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

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

Evidence

kernel-Nat.sumRange_permute

Kind: kernel-term
Status: checked

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

footprint-Nat.sumRange_permute

Kind: exhaustive-enumeration
Status: checked

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

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 the module's own test file.

numeric-permutation

Kind: exhaustive-enumeration
Status: checked

Supports: C5 of the ADR-1540 check script verifies the identity over EVERY permutation of [0,n) for n <= 6 (874 of them), not a sample; controls M4 and M5 refute the two ways of dropping a hypothesis -- the non-injective `sigma k := 0` gives 5 against 0, and the injective-but-escaping `sigma k := k+1` gives 5 against 14.

Checker command

python3 docs/research/09-decisions/adr-1540-eisenstein-side-and-sum-permute-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: 11 of 11 mutations (each claim inverted, each control's named witness moved or neutered, and the recorded survivor made to stop surviving) exit 1. One control, M6, is recorded as a DELIBERATE SURVIVOR and asserted to survive: swapping `a` and `b` throughout sumRange_point_change leaves a true statement, because the equation is symmetric in that swap. No numeric check can separate those two readings, which is why the declared type is pinned character for character in the module's test file.

Provenance

{
  "date": "2026-09-02",
  "curation": "curated",
  "established_by": "axeyum-lean-kernel build_nat_prelude (crates/axeyum-lean-kernel/src/nat_prelude/sum_range_permute.rs)",
  "source": "formal.statement and axiom_footprint are taken verbatim from the kernel's own rendering (nat_theorem_inventory, which is Kernel::render_lean of the admitted declaration type; the same string is pinned character for character by the module's the_family_states_the_intended_types test). depends_on is the direct-theorem column of theorem_dependency_inventory intersected with this ledger's registered facts. Nothing about the statement was hand transcribed; title, statement and the evidence notes were authored (lane eisenstein-lattice)."
}