Deleting a fixed set from every member of an indexed family commutes with taking the family's union, so the union loses at most that set's own size

Identifier: F:hall-union-under-family-deletion
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let nb be a family of finite sets of naturals indexed by the naturals, t a finite index set, and u a finite set. Throwing u out of every member of the family and then unioning over t gives the same set -- member for member, at every point -- as unioning over t and then throwing u out. Consequently the union of the deleted family is smaller than the original union by at most the size of u: card (unionOver nb t) <= card (unionOver (fun i => sdiff (nb i) u) t) + card u. Both statements are kernel terms with an empty axiom footprint. The additive form is the honest one here because Nat subtraction is truncated; the subtractive reading is the same statement and is vacuously weaker exactly when card u is large, which is the case the Hall argument cares about.

Formal statement

theorem Nat.Hall.card_le_card_unionOver_sdiff_add : ((x0 : ((x0 : AxNat) -> AxNat.Finset)) -> ((x1 : AxNat.Finset) -> ((x2 : AxNat.Finset) -> AxNat.le (AxNat.Finset.card (AxNat.Hall.unionOver x0 x2)) (AxNat.add (AxNat.Finset.card (AxNat.Hall.unionOver (fun (x3 : AxNat) => AxNat.Finset.sdiff (x0 x3) x1) x2)) (AxNat.Finset.card x1)))))

Dependencies

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

3 direct dependencies 4 direct dependents

Evidence

kernel-Nat.Hall.card_le_card_unionOver_sdiff_add

Kind: kernel-term
Status: checked

Supports: the union of the deleted family loses at most card u from the original union

Checker command

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

Evidence notes

ADR-1614 sized this step as a genuine counting argument over a union whose bound changes at every step. It is not: the deleted set does not depend on the index, so the quantifier commutes and the whole content is pointwise. The card follows in ONE application of Nat.Finset.card_congr_of_memB, and the only counting left is the single-deletion bound in finset.rs. The union's bound never enters -- bound (sdiff s u) IS bound s by iota, so the modified family has the same unionBound anyway.

kernel-Nat.Finset.card_le_card_sdiff_add

Kind: kernel-term
Status: checked

Supports: deleting a set from a finite set removes at most that set's own size

Checker command

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

Evidence notes

A plain Nat.Finset law, filed in finset.rs rather than hall.rs -- the same call ADR-1614 made for card_congr_of_memB. Everything is folded over the common bound `bound s + bound t`, where card_eq_countRange_add collapses each of the three counts back to its own card; `sdiff s t` is free there because its stored bound IS `bound s`. Between the folds sit two loose countRange facts that already existed: countRange_le_of_subset applied to `p subset (p \ q) union q` (pointwise, one Bool decision on q k), and countRange_union_add_inter read as an inequality by discarding the intersection through le_add_right. Before this lane NOTHING in the tree had a type mentioning Nat.Finset.sdiff.

eval-deletion-commutes-tight

Kind: instance-pin
Status: checked

Supports: the deletion really takes effect, and the bound is TIGHT rather than slack

Checker command

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

Evidence notes

nb 0 = {1,2}, nb 1 = {2,3}, index set {0,1}, deleted set u = {2}. The union is {1,2,3} (card 3); the union of the deleted family is {1} u {3} = {1,3} (card 2), and so is the deletion of the union. The deficiency bound is TIGHT here -- 3 <= 2 + 1 -- which is what makes the arithmetic discriminating: an off-by-one in either direction breaks it. The named wrong answer is 3, which is what a family modification that did NOT take effect would give.

shape-Nat.Hall.card_le_card_unionOver_sdiff_add

Kind: exhaustive-enumeration
Status: checked

Supports: the declarations exist under these exact names and are theorems, and nothing of this shape existed before

Checker command

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

Evidence notes

shape_search exits 1 when the count differs and 3 when the query is unanswerable, so a stale index cannot pass for a present declaration. The pre-state this row is measured against: at declarations=3000, positive control `--name Nat.Finset.forallSubset_of_search --expect 1` FOUND, `--const Nat.Finset.sdiff` returned ABSENT -- not one declaration in the tree had a type mentioning the set difference. The post-state is declarations=3017 on a binary rebuilt at this lane's HEAD, the increment being exactly the seventeen declarations added.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `hall-counting`, roadmap item W2-12 residue: `nat_prelude/hall.rs` gains `anyBelow_witness`, `memB_unionOver_elim`, both `unionOver` congruences and both family-modification transports; `nat_prelude/finset.rs` gains the set difference's membership calculus and `card_le_card_sdiff_add`. ADR-1623.",
  "source": "The deletion step of the standard inductive proof of Hall's marriage theorem, where the inductive hypothesis is applied to a family with a critical subfamily's union removed. Standard, and in a classical setting written as a subtraction over unions.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.sdiff_union_of_subset` and `Finset.card_sdiff`",
      "establishes": "the same deletion arithmetic over Mathlib's `Finset`, in the SUBTRACTIVE form and with decidable equality supplied by a typeclass; this route computes the carrier (a predicate plus a bound) so the difference needs no decidability instance, and states the count additively because `Nat.sub` is truncated"
    }
  ]
}