A sum indexed by the subsets of [0,n+1) splits into the subsets that omit n and the subsets that contain it, and over a predicate-valued subset that split is Eq.refl

Identifier: F:nat-subset-sum-split-law
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For every summand F : (Nat -> Bool) -> Nat and every width n, the sum of F over all subsets of [0, n+1) equals the sum over the subsets of [0,n) plus the sum over those same subsets with n inserted. Grading by cardinality parity, the same split holds with the parity FLIPPED on the half that gains an element, so the even and odd sums satisfy a coupled pair of recurrences. Both are Eq.refl, and that is the content of the fact rather than an incidental convenience: the enumeration is a fold over the WIDTH of a Nat -> Bool predicate, so the two halves of the split are literally the two branches of the fold's own recursion. Over the alternative enumeration -- ADR-1614's Nat.Finset.decode, which reads the subset off the bits of a code k < 2^n -- the same split has to cut the code range [0, 2^(n+1)) at 2^n and then prove testBit (2^n + k) i = testBit k i below n and testBit (2^n + k) n = 1, neither of which this prelude has. A Finset-valued enumeration cannot have a refl split law at ALL, because the carrier stores a bound and decode n k and decode (succ n) k are different terms for the same set.

Formal statement

theorem Nat.Subsets.sumSubsets_succ : ((x0 : ((x0 : ((x0 : AxNat) -> Bool)) -> AxNat)) -> ((x1 : AxNat) -> Eq.{1} AxNat (AxNat.Subsets.sumSubsets (AxNat.succ x1) x0) (AxNat.add (AxNat.Subsets.sumSubsets x1 x0) (AxNat.Subsets.sumSubsets x1 (fun (x2 : ((x2 : AxNat) -> Bool)) => x0 (AxNat.Subsets.insertAt x1 x2))))))

Dependencies

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

3 direct dependencies 2 direct dependents

Evidence

kernel-Nat.Subsets.sumSubsets_succ

Kind: kernel-term
Status: checked

Supports: the split law and its parity-graded twin, both admitted by the trusted gate

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::subset_sums_tests -- --test-threads=4

Evidence notes

Both laws are `Eq.refl`, so what the accept/reject pairs actually pin is the ORDER and the parity flip, neither of which `refl` can supply on its own. The split law is offered at a statement with its two halves exchanged and the graded one at a statement without the `notB`, and both must be REJECTED -- `Nat.add` recurses on its right argument, so at a symbolic `n` the two orders are different terms.

kernel-Nat.Subsets.sumSel_congr

Kind: kernel-term
Status: checked

Supports: two summands agreeing on the SUPPORTED predicates give equal graded sums -- the obligation a width-indexed summand incurs, stated rather than hidden

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::subset_sums_tests -- --test-threads=4

Evidence notes

`sumSel n F b` only ever applies `F` to predicates that are false at every index at or above `n`, so a summand built from a width (a product over [0,n), say) is free above it. This is the whole reason the width in `meetInd A n s v` can be moved independently of the fold's own width, which is what general inclusion-exclusion's induction step does.

eval-subset-sums-small

Kind: instance-pin
Status: checked

Supports: the fold visits every subset exactly once, in binary order, and grades the empty set as EVEN

Checker command

cargo test --release -p axeyum-lean-kernel --lib nat_prelude::subset_sums_tests -- --test-threads=4

Evidence notes

`sumSubsets 2 card = 0 + 1 + 1 + 2 = 4`, with `3` named as the answer a fold that dropped the without-n half gives and `6` as the answer a fold that visits {0,1} twice gives; `sumSubsets n (fun _ => 1) = 2^n` at n = 0,1,2,3. `sumSel 1 (fun s => if s 0 then 7 else 2) true = 2` and `... false = 7` -- these two are what the coordinated parity-flip mutant answers backwards. Widths stay at n <= 3 because every Nat numeral here is unary and the fold visits 2^n subsets.

shape-Nat.Subsets.sumSubsets

Kind: exhaustive-enumeration
Status: checked

Supports: nothing of this shape existed before

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --name Nat.sumDivisorsBy_reindex --expect 1

Evidence notes

Pre-state measured at declarations=3000 against a binary rebuilt at this lane's base commit, with the positive control FOUND 1 and exit 0. `--name-like` returned ABSENT for sumSubsets, subsetSum, evenB, isEven, withTop and Bool.or; it returned FOUND for testBit, setUnion, prodRangeIf and countRange_union_add_inter, which is why this module builds none of those.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `inclusion-exclusion-mobius`, roadmap item W2-19: `nat_prelude/subset_sums.rs`. ADR-1624.",
  "source": "Elementary. In a classical development the split is `Finset.powerset_succ` and nobody writes it down, because the powerset of an inductive type is a library primitive.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.sum_powerset_insert`",
      "establishes": "the same split over `Finset.powerset`, which needs the `Finset` quotient and a decidable-membership instance; this one is a fold over a `Nat -> Bool` predicate and closes by `Eq.refl`"
    }
  ]
}