Lax Lean Archive

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

Lax214022.CographWelzlUpperBound

Cographs have logarithmic Welzl orders

concepts/Lax214022/CographWelzlUpperBound.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

    Every cograph on n vertices has a Welzl order of crossing number at most 4∗(ceil(log2n)+1)4 * (ceil(log₂ n) + 1) for its open-neighborhood set system.

    The order is obtained from a cotree by recursively removing a heavy root-to-leaf path. The subtrees hanging from that path are ordered first at join nodes from the root downward and then at union nodes in the reverse direction. For a vertex in any one subtree, its neighbors in all the other subtrees occupy at most two intervals. Only the subtrees on the vertex's path through the recursive decomposition matter. The number of recursive levels is the Strahler rank of the cotree, which is at most the binary logarithm of its number of leaves.

    Lean source view on GitHub

    1import Lax214022.Cographs
    2import Lax195003.WelzlOrdersNeighborhoodSetSystem
    3import Mathlib.Data.Nat.Log
    4
    5/-!
    6---
    7title: Cographs have logarithmic Welzl orders
    8type: theorem
    9---
    10Every cograph on *n* vertices has a Welzl order of crossing number at most
    11`4 * (ceil(log₂ n) + 1)` for its open-neighborhood set system.
    12
    13The order is obtained from a cotree by recursively removing a heavy
    14root-to-leaf path. The subtrees hanging from that path are ordered first at
    15join nodes from the root downward and then at union nodes in the reverse
    16direction. For a vertex in any one subtree, its neighbors in all the other
    17subtrees occupy at most two intervals. Only the subtrees on the vertex's
    18path through the recursive decomposition matter. The number of recursive
    19levels is the Strahler rank of the cotree, which is at most the binary
    20logarithm of its number of leaves.
    21
    22# Formalization notes
    23
    24The ceiling logarithm is `Nat.clog 2 n`, matching the convention in the
    25Welzl-order submission. The additive one absorbs the two harmless endpoint
    26boundaries in the recursive construction. The statement is valid without a
    27nonemptiness hypothesis: at `n = 0` the unique order has crossing number zero.
    28-/
    29
    30namespace Lax214022.CographWelzlUpperBound
    31
    32open Lax195003.WelzlOrders
    33open Lax195003.WelzlOrdersNeighborhoodSetSystem
    34open Lax214022.Cographs
    35
    36/-- Every cograph has an open-neighborhood Welzl order with at most four
    37times one plus the ceiling binary logarithm of its order crossings. -/
    38axiom exists_welzlOrder_crossingNumber_le_four_clog_add_one
    39 (n : ℕ) (G : SimpleGraph (Fin n)) (hG : IsCograph G) :
    40 ∃ π : Equiv.Perm (Fin n),
    41 IsWelzlOrder (neighborhoodSetSystem G 1) π
    42 (4 * (Nat.clog 2 n + 1))
    43
    44end Lax214022.CographWelzlUpperBound
    45
    Show Proof

    Formalization notes

    The ceiling logarithm is Nat.clog2nNat.clog 2 n, matching the convention in the Welzl-order submission. The additive one absorbs the two harmless endpoint boundaries in the recursive construction. The statement is valid without a nonemptiness hypothesis: at n=0n = 0 the unique order has crossing number zero.

    Builds on

    Used by

    none

    From Mathlib

    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…