Rat.sumRange_matSkip: summing along the injection that misses j, plus f j, is the whole sum

Identifier: F:rat-sum-range-mat-skip
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, and Rat.matSkip j is the order-preserving injection [0,n) -> [0,n+1) whose image misses j. This fact records that if j <= n then sumRange (fun k => f (matSkip j k)) n + f j = sumRange f (succ n), for every f. In words: reindexing a sum by the injection that deletes index j, and then adding the deleted value back, recovers the sum over the full range. The hypothesis is necessary -- at j = 2, n = 1 the deleted index is outside the range, nothing is deleted, and adding f j over-counts; the identity fails at 180 of 400 random instances with j > n. This is the RANGE half of a Laplace expansion: a cofactor sum runs over a range one short, reindexed by matSkip, and this lemma is what fills it back to the full range so that a double cofactor expansion is a plain rectangle and the ordinary order-of-summation swap Rat.sumRange_swap applies, with no triangle decomposition and no Nat.sub.

Formal statement

theorem Rat.sumRange_matSkip : ((x0 : AxNat) -> ((x1 : ((x1 : AxNat) -> Rat)) -> ((x2 : AxNat) -> ((x3 : Eq.{1} Bool (AxNat.ble x2 x0) Bool.true) -> Eq.{1} Rat (Rat.add (Rat.sumRange (fun (x4 : AxNat) => x1 (Rat.matSkip x2 x4)) x0) (x1 x2)) (Rat.sumRange x1 (AxNat.succ x0))))))

Dependencies

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

5 direct dependencies 1 direct dependents

Evidence

kernel-Rat.sumRange_matSkip

Kind: kernel-term
Status: checked

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

Kind: exhaustive-enumeration
Status: checked

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

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-sumRange-matSkip-hypothesis-is-necessary

Kind: kernel-term
Status: checked

Supports: The ble hypothesis is load-bearing, and Rat.sumRange_peel_head's tail really is shifted -- both checked at ground instances differing in one index.

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, the identity holds at (j, n) = (2, 2) where ble 2 2 = true and FAILS at (2, 1) where ble 2 1 = false -- 1 against 0. Same def_eq call, one index apart. What it does NOT check: the ORDER of summation, any sign convention (there are no signs in this statement), and matSkip's branch order beyond a single shift.

control-adr-1155-numeric-sweep

Kind: exhaustive-enumeration
Status: checked

Supports: The identity holds at every sampled instance with j <= n and FAILS at 180 of 400 random instances with j > n, so the premise is not discardable.

Checker command

python3 docs/research/09-decisions/adr-1155-laplace-route-checks.py

Evidence notes

Simulates Rat.sumRange, Rat.matSkip and Rat.det over Fraction at the definitions rat_prelude/matrix_det.rs uses, exits 1 if any claim fails, and REQUIRES a nonzero count of counterexamples in the j > n region so that a discardable premise would be reported. Verified to fail: swapping the simulated matSkip's branches makes it exit 1 at the first control. Independent of the kernel proof.

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, against ADR-1135's third open law over the general-n determinant. Design note: ADR-1155."
}