Proof of `Exact rational search for a conditioning set` (2nd statement)
groundedproofs/Lax263307Proofs/RationalConditioning.lean · lax-263307
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds — checked by the archive's pipeline. Proof code is not displayed here.
Description
The fixed-order enumeration contains exactly the sets within the budget.
Proof strategy
A sublist of the vertex list has no duplicates, so its length equals the cardinality of its vertex set. Conversely, filter the vertex list by any given set and select that sublist at its cardinality.
Attribution
The finite enumeration used in Bonnet–Chang, proof of Lemma 12.