A finite set of naturals with a positive cardinality has a member, and the member is computed by a bounded search rather than chosen

Identifier: F:nat-finset-exists-memb-of-card-pos
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Let s be a Nat.Finset -- a decidable membership predicate together with a bound past which nothing is a member -- and suppose its cardinality is positive. Then there is an index k, strictly below s's own stored bound, at which membership decides true. Every other counting law in this kernel runs the other way, turning members into a count; this is the direction that turns a count back into a member, and it is what an induction that must pick an element out of a non-empty index set needs. There is no choice principle available here, so the witness is COMPUTED: the proof decides the bounded loop 'no index below the bound is a member' and reads a refuted loop through the existing search primitive. This is a kernel term with an empty axiom footprint.

Formal statement

theorem Nat.Finset.exists_memB_of_card_pos : ((x0 : AxNat.Finset) -> ((x1 : AxNat.lt AxNat.zero (AxNat.Finset.card x0)) -> Exists.{1} AxNat (fun (x2 : AxNat) => And (AxNat.lt x2 (AxNat.Finset.bound x0)) (Eq.{1} Bool (AxNat.Finset.memB x0 x2) Bool.true))))

Dependencies

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

5 direct dependencies 2 direct dependents

Evidence

kernel-Nat.Finset.exists_memB_of_card_pos

Kind: kernel-term
Status: checked

Supports: a positive cardinality yields a member below the set's own bound

Checker command

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

Evidence notes

The proof is a decision on the loop `allBelow (fun k => notB (memB s k)) (bound s)`. A `false` verdict is handed to `allBelow_false_witness`, whose index is re-introduced unchanged after `notB (memB s k) = false` is read back as membership. A `true` verdict says every index below the bound is a non-member, so `Nat.countRange_eq_zero_of_all_false` collapses `card s` to zero and the positivity hypothesis becomes `Lt zero zero`, refuted by `Nat.lt_irrefl`. Nothing anywhere chooses; the recursion inside `allBelow_false_witness` IS the search.

kernel-Nat.Finset.card_pos_of_memB

Kind: kernel-term
Status: checked

Supports: a member yields a positive cardinality -- the converse, and the direction that refutes membership when the count is zero

Checker command

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

Evidence notes

Much cheaper than the search direction because the witness is handed in: `lt_bound_of_memB` puts the index inside the counting range, `Nat.countRange_succ_of_true` peels it off as a `succ`, and `Nat.countRange_le_of_le` carries the resulting bound up to the set's own. `Lt i (bound s)` IS `Le (succ i) (bound s)` by delta, which is exactly `countRange_le_of_le`'s hypothesis, so there is no bridging step.

eval-Nat.Finset.empty

Kind: instance-pin
Status: checked

Supports: the new Definition `Nat.Finset.empty` really is the empty set and its bound really is zero

Checker command

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

Evidence notes

The trusted gate cannot tell a Definition is wrong: `Nat.Finset.range 7` has the type `Nat.Finset` just as `empty` does. So the term is reduced with the kernel's own def_eq and compared against hand-computed values, and every positive is paired with the wrong definition it rules out -- `mk (fun _ => false) 4` by the bound check, `Nat.Finset.range 0` by an explicit non-def-eq assertion. This test is load-bearing and was measured so: mutating `empty`'s stored predicate from `fun _ => false` to `fun _ => true` is ADMITTED by the kernel with the axiom sweep still green, and kills exactly one test, this one.

shape-absent-before

Kind: exhaustive-enumeration
Status: checked

Supports: this direction did not exist in the tree before this lane

Checker command

cargo run --release -q -p axeyum-lean-kernel --example shape_search -- --const Nat.Finset.singleton --min 1

Evidence notes

The binary was rebuilt at this lane's HEAD before the AFTER measurement; declarations went 3,093 -> 3,106, which is exactly the thirteen declarations the lane adds (one Definition, twelve Theorems), so the index is not stale in either direction. The positive control is of the same kind (a `Nat.Finset` operator that DOES carry lemmas), which is what makes the ABSENT reading a finding rather than a tool that was never pointed at the subject.

Provenance

{
  "date": "2026-09-05",
  "established_by": "axeyum lane `hall-singleton`, roadmap item W2-12: `nat_prelude/finset_singleton.rs`, a new module carrying `Nat.Finset.empty` and the singleton shelf alongside this lemma. ADR-1630.",
  "source": "The bottom of the standard inductive proof of Hall's marriage theorem, where the induction must produce an index of a non-empty index set before it can delete anything.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.card_pos` (`0 < s.card ↔ s.Nonempty`) and `Finset.Nonempty`",
      "establishes": "the same equivalence over `Finset`, where the underlying carrier is a `Multiset` with a nodup proof and nonemptiness is an existential over the list; the witness there comes out of the list structure, where this carrier has no list at all and must run a bounded decision to find one"
    }
  ]
}