Two families differing at one index have sums differing by that much

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

Recorded description

If `a` and `b` agree on `[0,n)` except possibly at `i0 < n`, then `sumRange a n + b i0 = sumRange b n + a i0`. WHY IT IS THE POINT: it is what replaces `Int.prodRange_swap`'s adjacent-transposition induction (three drafts, per `wilson.rs`) in the additive permutation argument. `sumRange` accumulates with `Nat.add`, so moving a value from slot `i0` up to slot `n` is one lemma rather than a transposition apparatus. STATED ADDITIVELY, not subtractively: `Nat.sub` is truncated, and the subtractive form would need a side condition this one does not. HOW IT IS PROVED: induction on `n` with the bound and both agreement hypotheses carried in the motive. `n = 0` is vacuous by `not_lt_zero`. At `succ j`, `lt_or_eq_of_le` splits `Le i0 j`: on `Lt i0 j` the induction hypothesis applies at `j` and the top index is off `i0`, so `a j = b j`; on `Eq i0 j` the top index IS `i0`, the two families agree everywhere below it, and `Nat.sumRange_congr_lt` equates the prefix sums. Each branch is four rewrites over one `add_assoc`/`add_comm` device. `Kernel::axiom_footprint` is EMPTY. Admitted by the trusted gate on the first attempt.

Formal statement

theorem Nat.sumRange_point_change : ((x0 : ((x0 : AxNat) -> AxNat)) -> ((x1 : ((x1 : AxNat) -> AxNat)) -> ((x2 : AxNat) -> ((x3 : AxNat) -> ((x4 : AxNat.lt x2 x3) -> ((x5 : ((x5 : AxNat) -> ((x6 : AxNat.lt x5 x2) -> Eq.{1} AxNat (x0 x5) (x1 x5)))) -> ((x6 : ((x6 : AxNat) -> ((x7 : AxNat.lt x2 x6) -> ((x8 : AxNat.lt x6 x3) -> Eq.{1} AxNat (x0 x6) (x1 x6))))) -> Eq.{1} AxNat (AxNat.add (AxNat.sumRange x0 x3) (x1 x2)) (AxNat.add (AxNat.sumRange x1 x3) (x0 x2)))))))))

Dependencies

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

8 direct dependencies 1 direct dependents

Evidence

kernel-Nat.sumRange_point_change

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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-point-change

Kind: exhaustive-enumeration
Status: checked

Supports: C4 of the ADR-1540 check script verifies the identity at 144 (n, i0, delta) cases; control M7 refutes the version without the one-index-differs hypothesis (two indices differing gives 25 against 20), and control M6 is recorded as a deliberate SURVIVOR.

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