Proof of `A class width bound obstructs induced route sampling` (1st statement)
groundedproofs/Lax263307Proofs/InducedEmbeddingWidth.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
Choose the proved induced almost-embedding with total route size at most 4M. The long-route count bounds L times the number of removed edges, and the pruning width bound gives the quantitative obstruction.