Hall's condition on a one-element index set produces a system of distinct representatives, with the representative computed from the count rather than chosen

Identifier: F:hall-base-case-singleton
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 suppose Hall's condition holds on the one-element index set {a}: every sub-family covers at least its own size. Then a system of distinct representatives for nb on {a} exists -- explicitly, the function constant at some member of nb a. This is Hall's marriage theorem at the bottom of its induction. The content is not the combinatorics but the extraction: Hall's condition is a COUNTING statement, saying only that the union of the family over {a} has at least one element, and turning that count back into a value needs a bounded search, since this kernel has no choice principle. Injectivity is free, because every index of a singleton is a. This is a kernel term with an empty axiom footprint.

Formal statement

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

Dependencies

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

3 direct dependencies 2 direct dependents

Evidence

kernel-Nat.Hall.exists_isMatching_singleton

Kind: kernel-term
Status: checked

Supports: Hall's condition at a singleton index set yields a matching

Checker command

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

Evidence notes

Hall's condition is instantiated at t := singleton a with the identity inclusion, giving Le (card (singleton a)) (card (unionOver nb (singleton a))). Nat.Finset.card_singleton rewrites the left side to `succ zero`, and `Nat.lt x y` is `Nat.le (succ x) y` by delta, so the count IS a positivity statement with no bridging lemma. Nat.Finset.exists_memB_of_card_pos then produces a value in the union, Nat.Hall.memB_unionOver_elim produces an index of the singleton at which the value is a member, and Nat.Finset.eq_of_memB_singleton identifies that index as a. The matching is the constant function at the value.

kernel-Nat.Hall.isMatching_congr

Kind: kernel-term
Status: checked

Supports: a matching depends only on the index set's members, never on its stored bound

Checker command

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

Evidence notes

The index-set twin of Nat.Hall.memB_unionOver_congr, and needed for the same reason: `Nat.Finset` carries a stored bound that extensionally equal sets need not share, so `union t (sdiff s t)` is not the same term as `s` even when it has the same members. Both IsMatching conjuncts mention the index set ONLY in hypothesis position, so unlike card_unionOver_congr this needs no counting at all -- it composes the pointwise equation with each incoming membership proof.

vocabulary-composes-with-necessity

Kind: exhaustive-enumeration
Status: checked

Supports: the base case is stated in necessity's vocabulary, so the two compose rather than merely coexisting

Checker command

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

Evidence notes

The test reads the rendered types of Nat.Hall.hallCondition_of_isMatching and of this theorem out of the kernel environment and requires both to mention Nat.Hall.IsMatching and Nat.Hall.HallCondition, and requires this one to mention Nat.Finset.singleton. The footprint sweep cannot see a vocabulary drift: a base case phrased over `Nat.Finset.range 1` would be equally axiom-free and equally useless for an induction on an arbitrary Nat.Finset.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `hall-singleton`, roadmap item W2-12: `nat_prelude/hall_sufficiency.rs`, a new module beside the existing `hall.rs` (which proves necessity). ADR-1630.",
  "source": "The base case of the standard inductive proof of Hall's marriage theorem.",
  "prior_art": [
    {
      "citation": "P. Hall, 'On Representatives of Subsets', J. London Math. Soc. 10 (1935) 26-30",
      "establishes": "the theorem; the one-set case is the trivial opening of the induction there, because a non-empty finite set is assumed to have an element without further argument"
    },
    {
      "citation": "Mathlib, `Finset.all_card_le_biUnion_card_iff_exists_injective`",
      "establishes": "the full theorem over `Finset` with classical choice available; the base case is discharged by `Finset.card_pos` plus `Finset.Nonempty.choose`, where this route must compute the representative"
    }
  ]
}