Proof of `A class width bound obstructs induced route sampling` (2nd 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
Restrict the host to the route union, which belongs to the class by heredity. Bound its induced edge count, apply the monotone class bag bound, and transfer back to the source with singleton bags for isolated vertices. An empty route union makes the source edgeless and gives bag size one.