Lax Lean Archive

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

Lax195003.WelzlOrdersInGraphs

Welzl orders in graphs

concepts/Lax195003/WelzlOrdersInGraphs.lean · lax-195003

definition

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

    Open claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Definition

    For a graph and a radius k, a graph Welzl order of crossing number at most ℓ is a Welzl order for the graph's open k-neighborhood set system. It is therefore crossed at most ℓ times by every open k-neighborhood.

    Lean source view on GitHub

    1import Lax195003.WelzlOrdersNeighborhoodSetSystem
    2
    3/-!
    4---
    5title: Welzl orders in graphs
    6type: definition
    7---
    8For a graph and a radius *k*, a graph Welzl order of crossing number at most
    9*ℓ* is a Welzl order for the graph's open *k*-neighborhood set system. It is
    10therefore crossed at most *ℓ* times by every open *k*-neighborhood.
    11
    12# Formalization notes
    13
    14The neighborhood set system and its bounded-walk definition are provided by
    15the separate `Lax195003.WelzlOrdersNeighborhoodSetSystem` concept. Its
    16radius-one instance is the ordinary open neighborhood system used by the graph
    17theorem.
    18
    19An algorithmic output is a list of vertices in increasing order. Rather than
    20introducing a separate generic encoding predicate, `EncodesGraphWelzlOrder`
    21states directly that the list represents some permutation which is a Welzl
    22order for the graph's `radius`-neighborhood system. It does not prescribe
    23which of the potentially many good orders an algorithm must choose.
    24-/
    25
    26namespace Lax195003.WelzlOrdersInGraphs
    27
    28open Lax195003.WelzlOrders
    29open Lax195003.WelzlOrdersNeighborhoodSetSystem
    30
    31/-- The word `y` encodes a Welzl order of crossing number at most
    32`crossingBound` for the `radius`-neighborhood set system of `G`. -/
    33def EncodesGraphWelzlOrder {n : ℕ} (G : SimpleGraph (Fin n))
    34 (radius crossingBound : ℕ) (y : List ℕ) : Prop :=
    35 ∃ π : Equiv.Perm (Fin n),
    36 y = List.ofFn (fun i : Fin n => (π.symm i).val) ∧
    37 IsWelzlOrder (neighborhoodSetSystem G radius) π crossingBound
    38
    39end Lax195003.WelzlOrdersInGraphs
    40

    Formalization notes

    The neighborhood set system and its bounded-walk definition are provided by the separate Lax195003.WelzlOrdersNeighborhoodSetSystemLax195003.WelzlOrdersNeighborhoodSetSystem concept. Its radius-one instance is the ordinary open neighborhood system used by the graph theorem.

    An algorithmic output is a list of vertices in increasing order. Rather than introducing a separate generic encoding predicate, EncodesGraphWelzlOrderEncodesGraphWelzlOrder states directly that the list represents some permutation which is a Welzl order for the graph's radiusradius-neighborhood system. It does not prescribe which of the potentially many good orders an algorithm must choose.

    Builds on

    Used by

    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…