Splitting a finite set of naturals at a subset splits its count exactly, so a nonempty proper part and its complement are both strictly smaller

Identifier: F:hall-descent-measure
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let s and t be finite sets of naturals with t a subset of s. Then card s = card t + card (s \ t) exactly. Consequently, if s \ t is nonempty then card t < card s, and if t is nonempty then card (s \ t) < card s. These are the two measures Hall's marriage theorem descends on: the inductive step splits the index set at a critical subset and recurses on both halves, and each half needs a strictly smaller count. The tree already carried the corresponding INEQUALITY, card s <= card (s \ t) + card t, which holds without the subset hypothesis and bounds card s from above -- the wrong direction for a descent. The content here is that for a genuine subset the two sides are equal, and that equality is what turns Nat.add_lt_add_left at the summand zero into a strict decrease. Stated over the decidable inclusion test Nat.Finset.subsetFixed with a bound side condition, because that is what the inductive step's subset search produces. These are kernel terms with empty axiom footprints.

Formal statement

theorem Nat.Finset.card_lt_card_of_subsetFixed : ((x0 : AxNat.Finset) -> ((x1 : AxNat.Finset) -> ((x2 : AxNat.le (AxNat.Finset.bound x1) (AxNat.Finset.bound x0)) -> ((x3 : Eq.{1} Bool (AxNat.Finset.subsetFixed x0 x1) Bool.true) -> ((x4 : AxNat.lt AxNat.zero (AxNat.Finset.card (AxNat.Finset.sdiff x0 x1))) -> AxNat.lt (AxNat.Finset.card x1) (AxNat.Finset.card x0))))))

Dependencies

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

4 direct dependencies 1 direct dependents

Evidence

kernel-Nat.Finset.card_lt_card_of_subsetFixed

Kind: kernel-term
Status: checked

Supports: a nonempty proper subset has a strictly smaller count

Checker command

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

Evidence notes

The proof is Nat.add_lt_add_left (card t) zero (card (sdiff s t)) applied to the positivity hypothesis, whose left side `add (card t) zero` IS `card t` by iota because Nat.add recurses on its RIGHT argument -- no add_zero rewrite appears in the term -- followed by one transport along Nat.Finset.card_add_card_sdiff. The mirror lemma costs one Nat.add_comm more, because add_lt_add_left grows the right summand and there the surviving one is on the left.

applied-type-is-strict-not-weak

Kind: exhaustive-enumeration
Status: checked

Supports: the measure is a STRICT inequality, checked on types the kernel compares rather than on a rendered statement

Checker command

cargo test --release -p axeyum-lean-kernel --lib -- nat_prelude::hall_descent_tests::the_subset_measure_conclusion_is_strict nat_prelude::hall_descent_tests::the_complement_measure_conclusion_is_strict --test-threads=4

Evidence notes

Each test APPLIES its lemma at a closed instance (s = range 3, t = singleton 1, every hypothesis discharged by reduction), infers the resulting type with the kernel's own `infer`, and requires it to be def-eq to `Lt 1 3` (respectively `Lt 2 3`). A rendered-string check could not do this: `Nat.lt a b` unfolds to `Nat.le (succ a) b`, so both relations print as themselves and neither name distinguishes them. A descent measure is the one place in an induction where a weakened relation type-checks everywhere it is BUILT and fails only where it is USED, which is why the guard is placed on the lemma rather than left to the consumer.

the-bound-hypothesis-is-what-makes-the-bridge-true

Kind: instance-pin
Status: checked

Supports: `Le (bound t) (bound s)` on the inclusion bridge is a genuine side condition, not bookkeeping

Checker command

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

Evidence notes

subsetFixed empty (singleton 0) reduces to `true` -- bound empty is 0, so the loop answers no index at all -- while 0 IS a member of singleton 0 and is NOT a member of empty. So Nat.Finset.memB_of_subsetFixed_of_bound_le would be FALSE without its bound hypothesis, and this instance is exactly the one that violates it: ble (bound (singleton 0)) (bound empty) is false. The test asserts all four of those reductions, so a lane that reads the hypothesis as bookkeeping gets a failing test rather than a kernel rejection it has to interpret.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `hall-assembly`, roadmap item W2-12: `nat_prelude/hall_descent.rs`, a new module beside `hall_theorem.rs`. ADR-1645.",
  "source": "ADR-1644 named the arithmetic of the two descent steps as the one place a surprise was still possible in Hall's assembly, and said neither should be assumed free. Measured: both are one identity plus one positivity fact.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.card_sdiff_add_card_eq_card`",
      "establishes": "the same split over `Finset` with decidable equality and set extensionality available, so the rebuilt union IS the original set and the count identity is a rewrite; here `Nat.Finset` carries a stored bound that `union t (sdiff s t)` does not share with `s`, so the identity has to run through `card_congr_of_memB`"
    },
    {
      "citation": "P. Hall, 'On Representatives of Subsets', J. London Math. Soc. 10 (1935) 26-30",
      "establishes": "the induction these measures serve; the descent is taken as evident there, as it is in every textbook treatment"
    }
  ]
}