Hall's marriage theorem: a finite family of finite sets has a system of distinct representatives if and only if every sub-family covers at least its own size

Identifier: F:hall-marriage-theorem
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, and let s be a finite index set. Then Hall's condition holds on s -- every subset t of s satisfies card t <= card (union over t of nb) -- if and only if there is a function f that sends each index of s to a member of its own set and is injective on s. That is Hall's marriage theorem, in both directions, as a single biconditional. The sufficiency direction is proved by strong induction on card s: an explicit bounded search decides whether some nonempty proper subset of s is critical, the critical branch matches that subset and its complement separately against a family with the critical neighbourhood deleted and glues the two, and the non-critical branch commits one index to a neighbour and recurses on the rest against a family with that one value deleted. There is no choice principle in this kernel, so every witness is computed. This is a kernel term with an empty axiom footprint.

Formal statement

theorem Nat.Hall.marriage_iff : ((x0 : AxNat.Finset) -> ((x1 : ((x1 : AxNat) -> AxNat.Finset)) -> Iff (AxNat.Hall.HallCondition x0 x1) (Exists.{1} (((x2 : AxNat) -> AxNat)) (fun (x2 : ((x2 : AxNat) -> AxNat)) => AxNat.Hall.IsMatching x0 x1 x2))))

Dependencies

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

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

Evidence

kernel-Nat.Hall.marriage_iff

Kind: kernel-term
Status: checked

Supports: Hall's condition and the existence of a system of distinct representatives are equivalent

Checker command

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

Evidence notes

The forward direction is Nat.Hall.sufficient; the backward direction is Nat.Hall.hallCondition_of_isMatching (ADR-1608) under one Exists.rec to name the matching. Both halves and all five supporting declarations are covered by the same footprint sweep, and each footprint assertion is preceded by Environment::contains, because an empty axiom footprint is also what a missing name returns.

the-statement-is-a-biconditional-not-something-weaker

Kind: exhaustive-enumeration
Status: checked

Supports: the admitted statement relates Hall's condition to an EXISTENTIAL over choice functions, in the right direction

Checker command

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

Evidence notes

The footprint sweep cannot see a statement drift: an Iff whose two sides were the same proposition, or whose right side quantified a FIXED choice function rather than existentially, would be admitted and axiom-free just as happily. The test reads the rendered type out of the kernel environment and requires Iff, Nat.Hall.HallCondition, Nat.Hall.IsMatching and Exists all to appear; it then reads Nat.Hall.sufficient's type and requires HallCondition to occur BEFORE Exists, so the implication is not the converse.

critical-b-decides-the-four-conjuncts-separately

Kind: exhaustive-enumeration
Status: checked

Supports: the search predicate computes the decision it claims to, with each conjunct load-bearing at a different instance

Checker command

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

Evidence notes

The kernel cannot tell a Definition is wrong: Nat.Hall.criticalB type-checks at Finset -> (Nat -> Finset) -> Finset -> Bool and so does `fun _ _ _ => true`. So it is reduced at closed arguments against hand-computed verdicts, one row per conjunct. The two `ble 1 ...` conjuncts are the two nonemptiness facts the two recursive calls need and they sit on OPPOSITE sides of the split: without `0 < card t` the branch fires at t = empty and recurses on sdiff s empty at the same count; without `0 < card (sdiff s t)` it fires at t = s and recurses on t at the same count. The second test asserts the four counts that make each accepted by the other's test, so the pair is shown not to be one condition written twice.

the-predicate-alone-does-not-imply-inclusion

Kind: instance-pin
Status: checked

Supports: the decision procedure's verdict is strictly weaker than the proposition it is named for, and the search's bound equation is what closes the gap

Checker command

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

Evidence notes

Nat.Hall.criticalB (range 3) nb (singleton 5) reduces to `true`, and 5 is not a member of range 3: Nat.Finset.subsetFixed loops to bound s and answers nothing about indices at or above it (ADR-1644's truncation asymmetry). So the verdict alone does not give the critical branch the inclusion it needs. The proof does not assume it -- Nat.Finset.existsSubset_of_search returns Eq Nat (bound t) (bound s) alongside the verdict, and it is that equation, fed to Nat.Finset.memB_of_subsetFixed_of_bound_le, that upgrades the decision to a pointwise inclusion. The test pins both halves rather than choosing an instance where the predicate happened to answer `false`, which would have hidden the hazard behind a green assertion.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `hall-assembly`, roadmap item W2-12, sixth and final slice: `nat_prelude/hall_marriage.rs`. ADR-1645, completing ADR-1608, ADR-1614, ADR-1623, ADR-1630 and ADR-1644.",
  "source": "The standard inductive proof, split on whether a nonempty proper subset of the index set is critical.",
  "prior_art": [
    {
      "citation": "P. Hall, 'On Representatives of Subsets', J. London Math. Soc. 10 (1935) 26-30",
      "establishes": "the theorem"
    },
    {
      "citation": "Mathlib, `Finset.all_card_le_biUnion_card_iff_exists_injective`",
      "establishes": "the theorem over `Finset` in Lean 4, with classical choice and set extensionality available; that proof selects a critical subset with `Classical.choice` over a decidable-but-unenumerated existential and identifies extensionally equal finsets, where this route must run an explicit bounded search over subsets and carry a stored bound that extensionally equal sets need not share"
    },
    {
      "citation": "M. Hall Jr., 'Distinct representatives of subsets', Bull. Amer. Math. Soc. 54 (1948) 922-926",
      "establishes": "the infinite-index version; not in scope here -- the statement proved is the finite one, with the index set a `Nat.Finset`"
    }
  ]
}