The subsets of an initial segment are exhaustively enumerable by a natural-number code, and a bounded search over that enumeration decides a membership-congruent property for every subset

Identifier: F:finset-subset-search-reflection
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

Every finite subset of {0, ..., n-1} is the set decoded from exactly one natural number below 2^n, and the decoding agrees with the original set at EVERY index -- above the width both are empty. Consequently a Bool-valued search over the 2^n codes decides any membership-congruent property of subsets in both directions: a positive verdict yields an actual subset with the property, and an exhausted search refutes the property for every subset of that width. Both directions are kernel terms with an empty axiom footprint, and the enumeration is COMPUTED -- there is no choice principle anywhere in the route.

Formal statement

theorem Nat.Finset.forallSubset_of_search : ((x0 : ((x0 : AxNat.Finset) -> Bool)) -> ((x1 : AxNat) -> ((x2 : ((x2 : AxNat.Finset) -> ((x3 : AxNat.Finset) -> ((x4 : ((x4 : AxNat) -> Eq.{1} Bool (AxNat.Finset.memB x2 x4) (AxNat.Finset.memB x3 x4))) -> Eq.{1} Bool (x0 x2) (x0 x3))))) -> ((x3 : Eq.{1} Bool (AxNat.Finset.anySubset x0 x1) Bool.false) -> ((x4 : AxNat.Finset) -> ((x5 : AxNat.le (AxNat.Finset.bound x4) x1) -> Eq.{1} Bool (x0 x4) Bool.false))))))

Dependencies

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

1 direct dependencies 2 direct dependents

Evidence

kernel-Nat.Finset.forallSubset_of_search

Kind: kernel-term
Status: checked

Supports: an exhausted search refutes the property for every subset of the searched width

Checker command

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

Evidence notes

The congruence premise is carried EXPLICITLY rather than hidden: two Nat.Finsets with the same members are not Eq at the carrier (it stores a raw predicate and a bound), so the verdict cannot travel from the enumerated representative `decode n (encode t n)` to the caller's own `t` without it. `Nat.Finset.card_congr_of_memB`, landed in the same diff, is what discharges the premise for a property phrased through `card` -- which is exactly the shape Hall's critical-subfamily test has.

kernel-Nat.Finset.memB_decode_encode

Kind: kernel-term
Status: checked

Supports: the enumeration is EXHAUSTIVE: every set with bound at most n has the same members as the set decoded from its own code, at every index

Checker command

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

Evidence notes

Stated at EVERY index rather than only below the width. Below it, `bitB_encodeFrom` plus `zero_add`; at or above it both sides are false, because `memB` truncates inside its own definition (ADR-1577) and so `memB_of_bound_le` holds of every Nat.Finset with no side condition. That is what makes the congruence premise statable without an index bound. `encodeFrom_lt_pow` supplies the other half -- every code really is below `pow 2 n`, so the search range is the right one.

eval-decode-encode-small

Kind: instance-pin
Status: checked

Supports: the enumeration is the one claimed -- binary order, index i into bit i, truncated at the width

Checker command

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

Evidence notes

The trusted gate cannot tell you a Definition is wrong -- a decoder reading the bits in the reverse order has exactly the same type. Each definition is therefore reduced at concrete small arguments with the wrong formula named: decode 2 k enumerates {}, {0}, {1}, {0,1}; card (decode 2 7) is 2 and NOT 3, which is what a decode that did not inherit memB's truncation would give; encode {0} is 1 and encode {1} is 2, each named as the other's wrong answer because a reversed bit order swaps precisely those two. Widths stay at n <= 3: every Nat numeral in this prelude is unary and the search range is pow 2 n.

shape-Nat.Finset.forallSubset_of_search

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.Finset.forallSubset_of_search --kind theorem --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=2832 with positive control Nat.Rado.IsRadoNumber FOUND, --name-like returned ABSENT for decode, encode, subsets, powerset, enumerate and bitAt -- and FOUND 15 for testBit, which is why this module reuses the existing Nat-valued bit decoder instead of building one.

Provenance

{
  "date": "2026-09-04",
  "established_by": "axeyum lane `hall-sufficiency`, roadmap item W2-12 residue: `nat_prelude/subset_search.rs` declares the enumeration and both reflection directions; `nat_prelude/finset.rs` gains `card_congr_of_memB`, the lemma a card-based property needs to discharge the congruence premise. ADR-1614.",
  "source": "The finite powerset as a decidable, exhaustively enumerable family; standard, and in a classical setting invisible because choice supplies the subset directly. ADR-1608 named its absence as the blocker on Hall's marriage theorem in a choice-free kernel.",
  "prior_art": [
    {
      "citation": "Mathlib, `Finset.powerset` and the decidable-exists instances over it",
      "establishes": "the same enumerate-and-decide capability over Mathlib's `Finset`, which is a quotient of lists by permutation and so needs `Quot.sound`; this route computes the carrier instead and has an empty axiom footprint"
    }
  ]
}