Proof of `A width obstruction from sparse costs and bounded route loads`
groundedproofs/Lax263307Proofs/CostSamplingObstruction.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
Apply the three cost-based sampling estimates. The target and sparsity thresholds bound the two interaction contributions by 1/8 each. The expected total route size is at most m*ell, which is positive. Invoke the proved sampled width obstruction with this value of M.