Lax Lean Archive

Draft — mutable and not usable as a dependency; its citation marks the draft state.

Lax214022.CographWelzlLowerBound

Cographs can require logarithmic Welzl orders

concepts/Lax214022/CographWelzlLowerBound.lean · lax-214022

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    Theorem

    For every nonnegative integer k, there is a cograph on at least 3k3^k and at most 4k4^k vertices such that every vertex order has crossing number at least k for the open-neighborhood set system. In particular, these graphs require at least one half of the binary logarithm of their order.

    The witnesses are the underlying graphs of the transitive closures of complete rooted ternary trees. One recursive step places a universal root over three disjoint copies of the preceding graph. In cotree language this adds a join node and a union node, so every two new cotree levels force one new crossing.

    Lean source view on GitHub

    1import Lax214022.Cographs
    2import Lax195003.WelzlOrdersNeighborhoodSetSystem
    3
    4/-!
    5---
    6title: Cographs can require logarithmic Welzl orders
    7type: theorem
    8---
    9For every nonnegative integer *k*, there is a cograph on at least `3^k` and
    10at most `4^k` vertices such that every vertex order has crossing number at
    11least *k* for the open-neighborhood set system. In particular, these graphs
    12require at least one half of the binary logarithm of their order.
    13
    14The witnesses are the underlying graphs of the transitive closures of
    15complete rooted ternary trees. One recursive step places a universal root
    16over three disjoint copies of the preceding graph. In cotree language this
    17adds a join node and a union node, so every two new cotree levels force one
    18new crossing.
    19
    20# Formalization notes
    21
    22The two exponential inequalities state the logarithmic relation without
    23introducing rounded real logarithms. The theorem uses the registered
    24crossing number directly, at radius one. Thus it asserts a lower bound for
    25every permutation, rather than merely exhibiting one order with a large
    26crossing number.
    27-/
    28
    29namespace Lax214022.CographWelzlLowerBound
    30
    31open Lax195003.WelzlOrders
    32open Lax195003.WelzlOrdersNeighborhoodSetSystem
    33open Lax214022.Cographs
    34
    35/-- There are cographs of order at most `4^k` on which every Welzl order has
    36crossing number at least `k`. -/
    37axiom exists_cograph_requiring_crossingNumber_at_least (k : ℕ) :
    38 ∃ n : ℕ, 3 ^ k ≤ n ∧ n ≤ 4 ^ k ∧
    39 ∃ G : SimpleGraph (Fin n), IsCograph G ∧
    40 ∀ π : Equiv.Perm (Fin n),
    41 k ≤ crossingNumber (neighborhoodSetSystem G 1) π
    42
    43end Lax214022.CographWelzlLowerBound
    44
    Show Proof

    Formalization notes

    The two exponential inequalities state the logarithmic relation without introducing rounded real logarithms. The theorem uses the registered crossing number directly, at radius one. Thus it asserts a lower bound for every permutation, rather than merely exhibiting one order with a large crossing number.

    Builds on

    Used by

    none

    From Mathlib

    none

    Community review

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.

    0 comments

    Loading discussion…