Proof of `Computing the recursive answer-or-cut decision`
groundedproofs/Lax263307Proofs/ComputedRounding.lean · lax-263307
What this proof establishes
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
Inspect the actual first failed query. Its certified independence bound and rational target give the buffered component gap. If no query fails, skipped parts contribute the empty set and the successful answers satisfy the proved heavy-part union bound.