Lax Lean Archive

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

Refined near-linear computation of Welzl orders

Lax457868.RefinedWelzlOrders · concepts/Lax457868/RefinedWelzlOrders.lean · lax-457868

open

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

    For every graph with linear neighborhood complexity bounded by c⋅kc · k, where c≥2c ≥ 2, a randomized word-RAM algorithm computes an order whose crossing number is at most a constant times c5(log2c)2log2nc^5 (log₂ c)^2 log₂ n. Its running time is linear in the encoded input size times lognlog n, and it succeeds with probability at least 2/32/3. For fixed cc, the crossing bound is O(logn)O(log n).

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

    Each proof establishes this claim relative to its assumptions.

    No proof in the archive yet — this claim is open.

    Lean source view on GitHub

    1import Lax195003.WelzlOrdersInGraphs
    2import Lax195003.WelzlOrdersComputation
    3import Lax195003.WelzlOrdersNeighborhoodComplexity
    4import Lax195003.WordRamRandomness
    5import Lax11.GraphEncoding
    6import Lax808846.Ram
    7import Mathlib.Data.Nat.Log
    8
    9/-!
    10---
    11title: Refined near-linear computation of Welzl orders
    12type: theorem
    13---
    14For every graph with linear neighborhood complexity bounded by `c · k`,
    15where `c ≥ 2`, a randomized word-RAM algorithm computes an order whose
    16crossing number is at most a constant times
    17`c^5 (log₂ c)^2 log₂ n`. Its running time is linear in the encoded input
    18size times `log n`, and it succeeds with probability at least `2/3`.
    19For fixed `c`, the crossing bound is `O(log n)`.
    20
    21# Formalization notes
    22
    23The graph order and neighborhood-complexity predicates, the compressed-sparse-
    24row input encoding, and the finite-tape randomized word-RAM semantics are
    25imported from Lax195003 and its registered dependencies. The graph statement
    26uses the existing open-neighborhood convention. The paper's set-system result
    27implies this specialization because an undirected graph's open-neighborhood
    28system is self-dual.
    29
    30The paper states expected running time. This statement uses a bounded-time
    31version: truncate an expected-time run at a sufficiently large constant
    32multiple of its expectation and return failure on timeout. Markov's inequality
    33then gives success on at least two thirds of finite tapes, with every tape
    34halting within the displayed bound. Repeating independent attempts until a
    35valid order is returned recovers expected near-linear time. The runtime
    36constant is existential; the displayed crossing constant is an explicit
    37rounding-up of the paper's sampler parameters.
    38
    39The program is existential and black-box at the concept level. Its concrete
    40instruction sequence and the bridges from the refined sampler to the machine
    41interface belong in the proof package.
    42-/
    43
    44namespace Lax457868.RefinedWelzlOrders
    45
    46open Lax11.GraphEncoding
    47open Lax808846.Ram
    48open Lax195003.WelzlOrdersInGraphs
    49open Lax195003.WelzlOrdersNeighborhoodComplexity
    50open Lax195003.WordRamRandomness
    51
    52/-- A black-box word-RAM program achieves the refined crossing bound within
    53near-linear time, with constant success probability. -/
    54axiom exists_refined_randomized_welzlOrder_program :
    55 ∃ (p : Program) (Ktime : ℕ), 1 ≤ Ktime ∧
    56 ∀ (c n : ℕ) (G : SimpleGraph (Fin n)),
    57 2 ≤ c → 2 ≤ n →
    58 HasLinearNeighborhoodComplexityWithConstant G c →
    59 ∀ (w : ℕ) (x : List ℕ), EncodesGraph x n G →
    60 (∀ v ∈ c :: x, Ktime * (x.length + v + 1) ≤ 2 ^ w) →
    61 let T := Ktime * (x.length + 1) * (Nat.clog 2 n + 1)
    62 SucceedsWithProbabilityAtLeastInTime
    63 (2 / 3 : ℚ) w p (c :: x) T T
    64 (EncodesGraphWelzlOrder G 1
    65 (100000 * c ^ 5 * (Nat.clog 2 c + 1) ^ 2 *
    66 (Nat.clog 2 n + 1)))
    67
    68end Lax457868.RefinedWelzlOrders
    69
    Formalization notes

    The graph order and neighborhood-complexity predicates, the compressed-sparse- row input encoding, and the finite-tape randomized word-RAM semantics are imported from Lax195003 and its registered dependencies. The graph statement uses the existing open-neighborhood convention. The paper's set-system result implies this specialization because an undirected graph's open-neighborhood system is self-dual.

    The paper states expected running time. This statement uses a bounded-time version: truncate an expected-time run at a sufficiently large constant multiple of its expectation and return failure on timeout. Markov's inequality then gives success on at least two thirds of finite tapes, with every tape halting within the displayed bound. Repeating independent attempts until a valid order is returned recovers expected near-linear time. The runtime constant is existential; the displayed crossing constant is an explicit rounding-up of the paper's sampler parameters.

    The program is existential and black-box at the concept level. Its concrete instruction sequence and the bridges from the refined sampler to the machine interface belong in the proof package.

    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…