Proof of `Controlled-size subcubic source graphs of linear treewidth`
groundedproofs/Lax263307Proofs/SourceGraphs.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
Use the registered graph at its specified size selector. Its registered size, degree, and treewidth claims give all three bounds for the same graph. The size constant is positive because the size-one request is met. Prove positivity through generic arithmetic lemmas, leaving the fixed enormous seed degree symbolic rather than evaluating its numeral.