Proof of `Few edges in the graph induced by short routes`
groundedproofs/Lax263307Proofs/InducedRouteEdges.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
For each host vertex choose a route using it. All of its neighbors in the route union lie on routes incident to this chosen source edge, since the almost-embedding is induced. There are at most such routes and each has at most vertices. Combine this degree bound with the route-union order bound and the degree-sum formula.
Attribution
Bonnet–Chang, edge-count estimate in Lemma 11.