Rat.sumRange_peel_head: a finite sum is its first summand plus the shifted sum of the rest

Identifier: F:rat-sum-range-peel-head
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Rat.sumRange f n is the finite sum of f over [0,n) in the constructed rationals, defined by structural Nat.rec on the bound, so that sumRange f 0 = 0 and sumRange f (j+1) = sumRange f j + f j. The recursion peels from the RIGHT, so its defining equations give the LAST summand and nothing in this prelude gives the first. This fact records the left-hand peel: sumRange f (succ n) = f 0 + sumRange (fun k => f (succ k)) n, for every f and n, with no hypothesis. It generalises F:rat-sum-range-head-of-tail-zero, which reaches only the special case where every summand past index 0 vanishes, and it is what every left-side reindexing over Rat.sumRange needs -- F:rat-sum-range-mat-skip uses it three times.

Formal statement

theorem Rat.sumRange_peel_head : ((x0 : ((x0 : AxNat) -> Rat)) -> ((x1 : AxNat) -> Eq.{1} Rat (Rat.sumRange x0 (AxNat.succ x1)) (Rat.add (x0 AxNat.zero) (Rat.sumRange (fun (x2 : AxNat) => x0 (AxNat.succ x2)) x1))))

Dependencies

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

2 direct dependencies 2 direct dependents

Evidence

kernel-Rat.sumRange_peel_head

Kind: kernel-term
Status: checked

Supports: Rat.sumRange_peel_head 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 -- Rat.sumRange_peel_head 2>/dev/null | grep -cE '^Rat\.sumRange_peel_head[[: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. grep -c rather than grep -q, which would SIGPIPE the producer under pipefail. Pass ONE name per invocation. --release is MANDATORY.

footprint-Rat.sumRange_peel_head

Kind: exhaustive-enumeration
Status: checked

Supports: axiom_footprint: [] -- the rat prelude's trusted surface is empty, which bounds Rat.sumRange_peel_head.

Checker command

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

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.

control-the-tail-must-be-shifted

Kind: kernel-term
Status: checked

Supports: The tail's index shift is load-bearing: dropping it makes the statement false at a ground witness, while the stated form is true there.

Checker command

cargo test -p axeyum-lean-kernel --lib the_laplace_index_layer_hypotheses_are_load_bearing 2>&1 | grep -cE '^test result: ok\. 1 passed'

Evidence notes

The count is tested, not just the exit status: `1 passed` fails if the test is renamed away or filtered out. Against a row of Rat.matId that is nonzero at exactly index 2, sumRange f 3 is def_eq to f 0 + sumRange (fun k => f (succ k)) 2 (both 1) and is NOT def_eq to f 0 + sumRange f 2 (which is 0). What it does NOT check: the head itself, which is 0 for this f, and no sign convention -- there are no signs in this statement.

Provenance

{
  "date": "2026-08-31",
  "established_by": "axeyum-lean-kernel build_rat_prelude (crates/axeyum-lean-kernel/src/rat_prelude/matrix_det.rs)",
  "source": "Lane det-row-expansion, built as the prerequisite for F:rat-sum-range-mat-skip. Design note: ADR-1155."
}