General inclusion-exclusion for a finite family of decidable subsets, as two Nat sums rather than one signed one, and the two-set case is the pre-existing lemma verbatim

Identifier: F:nat-inclusion-exclusion-general
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let A be a family of decidable subsets of the ambient range [0,m), indexed by i < n. Write ieSumPos A n m b for the sum of the cardinalities of the intersections of the NON-EMPTY subfamilies whose index set has cardinality parity b. Then the cardinality of the union plus the even sum equals the odd sum: |union| + ieSumPos true = ieSumPos false. Nat has no negatives, so the classical alternating sum is stated as this pair of Nat sums; the ungraded form ieSum true + |union| = ieSum false + m is the same identity before the empty subfamily's contribution -- exactly m, the whole ambient range -- is cancelled off both sides. At n = 2 the theorem specialises to countRange (setUnion (A 0) (A 1)) m + countRange (setInter (A 0) (A 1)) m = countRange (A 0) m + countRange (A 1) m, which is Nat.countRange_union_add_inter's statement; that specialisation is a declared theorem, not a resemblance.

Formal statement

theorem Nat.Subsets.inclusion_exclusion_pos : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> Bool))) -> ((x1 : AxNat) -> ((x2 : AxNat) -> Eq.{1} AxNat (AxNat.add (AxNat.countRange (AxNat.Subsets.unionAt x0 x1) x2) (AxNat.Subsets.ieSumPos x0 x1 x2 Bool.true)) (AxNat.Subsets.ieSumPos x0 x1 x2 Bool.false))))

Dependencies

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

11 direct dependencies 0 direct dependents Graph shows the first 8 on each side.

Evidence

kernel-Nat.Subsets.inclusion_exclusion_pos

Kind: kernel-term
Status: checked

Supports: the classical statement, over the non-empty subfamilies, admitted by the trusted gate with an empty axiom footprint

Checker command

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

Evidence notes

The proof is `sumSel_swap` (turning the sum over subsets of a sum over elements inside out), then `sumSel_meetInd` at each ambient element, then `prodPar_even`, then `countRange_compl` to convert the residue into m minus the union's size without writing a subtraction. The graded pair is what makes the last step possible in Nat.

kernel-Nat.Subsets.inclusion_exclusion_two

Kind: kernel-term
Status: checked

Supports: the two-set case is recovered EXACTLY, and the recovery is checked by the kernel rather than asserted

Checker command

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

Evidence notes

The test builds the statement ONCE and offers it to the trusted gate TWICE: once with the derived theorem and once with `Nat.countRange_union_add_inter` applied at `A 0` and `A 1`. Both are admitted, so the two are the same type -- not two similar-looking renderings that a reader would have to compare by eye. The specialisations the kernel performs unaided: `unionAt A 2 v` IS `setUnion (A 0) (A 1) v`, because `anyOf`'s base case is the literal `false` that collapses a one-element union.

eval-three-explicit-sets

Kind: instance-pin
Status: checked

Supports: the theorem's numbers are the right numbers at a worked three-set instance, subset by subset

Checker command

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

Evidence notes

A i = {i, i+1} over [0,4), so A 0 = {0,1}, A 1 = {1,2}, A 2 = {2,3}. All EIGHT subset intersections are asserted separately -- 4, 2, 2, 2, 1, 0, 1, 0 -- because a meetInd that intersected the wrong subfamily can still make the totals agree. The union has 4 elements, the odd sum is 6, the even sum is 2, and 4 + 2 = 6.

kernel-Nat.Subsets.prodPar_even

Kind: kernel-term
Status: checked

Supports: the per-element alternating identity, which is the whole argument before it is summed over the range

Checker command

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

Evidence notes

One induction on the width and one Bool dichotomy on the new element: when it is IN, the residue is multiplied by 0 and the two graded halves exchange; when it is OUT, both halves and the residue are unchanged. No hypothesis is needed at all, because the family is Bool-valued and the indicator is 0 or 1 by construction rather than by assumption.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `inclusion-exclusion-mobius`, roadmap item W2-19: `nat_prelude/inclusion_exclusion.rs`. ADR-1624.",
  "source": "Classical (da Silva / Sylvester). The constructive content here is entirely in the encoding: no negatives, no Finset quotient, and no choice.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.inclusion_exclusion_card_biUnion`",
      "establishes": "the same theorem over an additive commutative GROUP, where the alternating sign is a ring element; this one is over Nat and therefore has to be a pair of sums, and its two-set case is the pre-existing Nat lemma"
    }
  ]
}