Proof of `A counterexample to Hadwiger's conjecture` (2nd statement)
groundedproofs/Lax342547Proofs/Construction.lean · lax-342547
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
The complete binary-frame construction produces graphs of arbitrarily large order. Its touching-matching number is the archive's matching number by definitional equality, and the strict rational bound gives the integral bound.