The alternating sum of a constant over the subsets of a NON-EMPTY ground set vanishes, and in Nat's graded form that is add_comm

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

Recorded description

For every constant c and every width n, the sum of c over the even-cardinality subsets of [0, n+1) equals the sum over the odd-cardinality subsets. Classically this is the statement that the alternating sum of the binomial coefficients of a non-empty row is zero; here Nat has no negatives, so it is stated as an equality between two Nat sums. The proof is one application of add_comm and nothing else, because the split law sends the even sum at width n+1 to (even at n) + (odd at n) and the odd sum to (odd at n) + (even at n), and a constant summand is unchanged by inserting an element. That the identity costs one lemma is the return on making the split law Eq.refl. Non-emptiness is not a side condition bolted on: the statement is over succ n, and at width 0 it is false (the only subset is empty, and it is even).

Formal statement

theorem Nat.Subsets.sumSel_const : ((x0 : AxNat) -> ((x1 : AxNat) -> Eq.{1} AxNat (AxNat.Subsets.sumSel (AxNat.succ x1) (fun (x2 : ((x2 : AxNat) -> Bool)) => x0) Bool.true) (AxNat.Subsets.sumSel (AxNat.succ x1) (fun (x2 : ((x2 : AxNat) -> Bool)) => x0) Bool.false)))

Dependencies

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

3 direct dependencies 0 direct dependents

Evidence

kernel-Nat.Subsets.sumSel_const

Kind: kernel-term
Status: checked

Supports: the even and odd sums of a constant over a non-empty ground set are equal

Checker command

cargo run --release -q -p axeyum-lean-kernel --example nat_theorem_inventory -- Subsets.sumSel_const

Evidence notes

The whole proof term is `Nat.add_comm (sumSel n K true) (sumSel n K false)`, offered at a statement about `succ n`. The kernel accepts it because both sides of the goal delta-reduce to the two orders of that sum -- the split law's `Eq.refl` doing the work -- and `(fun _ => c) o insertAt n` is `fun _ => c` by beta.

eval-parity-halves

Kind: instance-pin
Status: checked

Supports: the two halves really are the even and odd subsets, at widths where both can be listed

Checker command

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

Evidence notes

At width 2 over the indicator of {0,1} the even sum is 1 (only {0,1} contains both) and the odd sum is 0; over the constant 1 restricted to non-empty subsets the even sum is 1 and the odd sum is 2, which is the 1 + 2 = 3 non-empty subsets of a two-element set split by parity.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `inclusion-exclusion-mobius`, roadmap item W2-19 and the W2-18 residue: `nat_prelude/subset_sums.rs`. ADR-1624.",
  "source": "Classical: the alternating binomial row sum, (1 - 1)^n = 0 for n > 0.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.sum_pow_mul_eq_max_pow` / `Int.alternating_sum_range_choose`",
      "establishes": "the signed form over Int; the graded Nat form is what this build position can state, and it is the one Moebius inversion consumes"
    }
  ]
}