Proof of `Sublinear bag bounds survive independent blow-ups` (2nd statement)
groundedproofs/Lax263307Proofs/BlowUpBagBounds.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 base graph to used projection fibres, retaining class membership. One representative per fibre embeds it into the given blow-up and bounds its edge count. Enumerate the fibres to form an explicit copy-graph isomorphism. Apply degree-deletion optimization to its base decomposition and pull the resulting bags through that isomorphism.