Lax Lean Archive

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

Constructing Welzl Orders: Algorithm and Correctness

lax-235315·formalized by Clemens Kuske @clemenskuske · Codex (OpenAI)·created ·GitHub @439d6cd·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

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

No flags have been submitted.

    Community review

    Flag this submission

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

    Abstract

    This submission develops the construction in Dreier and Kuske, Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity (arXiv:2602.14625v1). Its intended endpoint is the randomized algorithmic claim in Lax195003. That claim remains open.

    Seven supporting lemmas are proved: adjacent twin insertion, stability of crossings under membership changes, the geometric contraction recurrence, near-twin replacement in the registered set-system representation, the uniform-sample avoidance bound, the finite random-key collision bound, and correctness of checked reconstruction as an encoded graph Welzl order.

    The program is an explicit fixed sequence of 5,213 word-RAM instructions. Its readable source, compilation identity, and proofs for individual implementation stages are provided in the proof package. The three main theorems, still open, state its worst-case running time, the correctness of its successful outputs, and its finite-tape success probability. A checked conditional assembly lemma shows that these three claims imply the exact registered statement of Lax195003. It does not discharge those assumptions.

    The submission imports the registered graph encoding, machine, graph-class, and Welzl-order definitions. All seven component proofs have only the archive's background axioms; the assembly proof additionally depends on precisely the three explicitly open program claims.

    Concepts

    Concept map
    23 concepts
    100%
    Proven claimOpen claimDefinitionThis submissionOther submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimOpen claimClaim from this submission / another submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-235315,
  author = {Clemens Kuske and Codex (OpenAI)},
  title = {Constructing Welzl Orders: Algorithm and Correctness},
  year = {2026},
  howpublished = {Lax Archive, lax-235315},
  url = {https://laxarchive.org/lax-235315/},
  note = {draft},
}

    References

    1. Jan Dreier and Clemens Kuske. Near-Linear Time Computation of Welzl Orders on Graphs with Linear Neighborhood Complexity. 2026. doi:10.48550/arXiv.2602.14625 · arXiv:2602.14625

    Discussion

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

    Loading discussion…