Lax Lean Archive

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

Reconstruction yields a graph Welzl order

Lax235315.ReconstructionCorrectness · concepts/Lax235315/ReconstructionCorrectness.lean · lax-235315

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.

    Natural Language Statement

    Lemma

    A checked reconstruction with r rounds, near-twin distance at most k, and a base ground set of size at most q returns a graph Welzl order with crossing number at most (r+1)q, provided 2k≤q.

    Taking k=6c²L, q=12c²L, and r+1≤L gives 12c²L², the deterministic crossing argument in Theorem 3.2 of Dreier–Kuske.

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

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax235315.TwinReconstruction
    2import Lax195003.WelzlOrdersInGraphs
    3
    4/-!
    5---
    6title: Reconstruction yields a graph Welzl order
    7type: lemma
    8---
    9A checked reconstruction with r rounds, near-twin distance at most k,
    10and a base ground set of size at most q returns a graph Welzl order with
    11crossing number at most (r+1)q, provided 2k≤q.
    12
    13Taking k=6c²L, q=12c²L, and r+1≤L gives 12c²L², the deterministic
    14crossing argument in Theorem 3.2 of Dreier--Kuske.
    15
    16# Formalization notes
    17
    18The output uses the exact registered graph-order relation, not a surrogate
    19list bound. The result proves both permutation validity and the crossing
    20bound. It is conditional on a concrete reconstruction certificate; producing
    21that certificate from machine execution is a separate open obligation.
    22-/
    23
    24namespace Lax235315.ReconstructionCorrectness
    25open Lax235315.TwinReconstruction Lax195003.WelzlOrdersInGraphs
    26
    27/-- A full-vertex reconstruction encodes an order with the accumulated crossing bound. -/
    28axiom encodesGraphWelzlOrder {n k q rounds bound : ℕ}
    29 (G : SimpleGraph (Fin n)) (l : List (Fin n))
    30 (h : Run G k q rounds Set.univ Set.univ l)
    31 (hkq : 2 * k ≤ q) (hbound : (rounds + 1) * q ≤ bound) :
    32 EncodesGraphWelzlOrder G 1 bound (l.map Fin.val)
    33
    34end Lax235315.ReconstructionCorrectness
    35
    Show Proof
    Formalization notes

    The output uses the exact registered graph-order relation, not a surrogate list bound. The result proves both permutation validity and the crossing bound. It is conditional on a concrete reconstruction certificate; producing that certificate from machine execution is a separate open obligation.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…