Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

A counterexample to Hadwiger's conjecture

Lax342547.Counterexample · concepts/Lax342547/Counterexample.lean · lax-342547

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Theorem 1.1 asserts that graphs of arbitrarily large order mm have independence number at most two and connected-matching number less than m/100m/100. Together with Proposition 3.5, this gives graphs of arbitrarily large order with h(G)<χ(G)h(G)<\chi(G).

    The proof package establishes the existence assertion by the complete binary-frame construction, and derives the coloring consequences from it.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 arbitrarily_large_hadwiger_counterexample proven

    2 arbitrarily_large_small_connected_matching proven

    Lean source view on GitHub

    1import Lax342547.ConnectedMatching
    2import Lax342547.CliqueMinor
    3import Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
    4
    5/-!
    6---
    7title: A counterexample to Hadwiger's conjecture
    8type: theorem
    9---
    10Theorem 1.1 asserts that graphs of arbitrarily large order mm have
    11independence number at most two and connected-matching number less than
    12m/100m/100. Together with Proposition 3.5, this gives graphs of arbitrarily
    13large order with h(G)<χ(G)h(G)<\chi(G).
    14
    15The proof package establishes the existence assertion by the complete
    16binary-frame construction, and derives the coloring consequences from it.
    17-/
    18
    19namespace Lax342547.Counterexample
    20
    21open ConnectedMatching CliqueMinor
    22
    23/-- Theorem 1.1, with the strict matching bound expressed in natural numbers. -/
    24axiom arbitrarily_large_small_connected_matching (lowerBound : ℕ) :
    25 ∃ m : ℕ, lowerBound ≤ m ∧ ∃ G : SimpleGraph (Fin m),
    26 G.indepNum ≤ 2 ∧ 100 * connectedMatchingNumber G < m
    27
    28/-- The ordinary coloring consequence of Theorem 1.1. -/
    29axiom arbitrarily_large_hadwiger_counterexample (lowerBound : ℕ) :
    30 ∃ m : ℕ, lowerBound ≤ m ∧ 5 ≤ m ∧ ∃ G : SimpleGraph (Fin m),
    31 G.indepNum ≤ 2 ∧ hadwigerNumber G < G.chromaticNumber.toNat
    32
    33end Lax342547.Counterexample
    34
    Show ProofShow Proof
    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…