Lax Lean Archive

The unoptimized empty-hexagon bound

Lax570090.HujterKisfaludiBak · concepts/Lax570090/HujterKisfaludiBak.lean · lax-570090

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

    Definition

    This module states the upper bound h(6)≤2428+1h(6) ≤ 2^428 + 1 and the ordered hexagon definitions used by the blocking argument. The bound is proved in Lax570090Proofs.EmptyHexagonLax570090Proofs.EmptyHexagon from Valtr's four-layer lemma. The visibility-colouring theorem is proved in Lax570090Proofs.HujterKisfaludiBakLax570090Proofs.HujterKisfaludiBak.

    Concept map
    2 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 Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
    2import Mathlib.Analysis.Convex.Hull
    3import Lax570090.Geometry
    4
    5/-!
    6---
    7title: The unoptimized empty-hexagon bound
    8type: definition
    9---
    10This module states the upper bound `h(6) ≤ 2^428 + 1` and the ordered hexagon
    11definitions used by the blocking argument. The bound is proved in
    12`Lax570090Proofs.EmptyHexagon` from Valtr's four-layer lemma. The visibility-colouring
    13theorem is proved in `Lax570090Proofs.HujterKisfaludiBak`.
    14-/
    15
    16namespace Lax570090.HujterKisfaludiBak
    17
    18open Lax570090.Geometry
    19
    20/-- Six labelled vertices in strict counterclockwise cyclic convex position.
    21
    22The last conjunct records the complete cyclic order type, not merely its six
    23supporting-edge consequences. This is useful in the direct geometric proof:
    24an increasing triple of cyclic labels is positively oriented. -/
    25def StrictConvexHexagon (h : Fin 6 → Point) : Prop :=
    26 Function.Injective h ∧
    27 (∀ i j : Fin 6, j ≠ i → j ≠ i + 1 →
    28 0 < turn (h i) (h (i + 1)) (h j)) ∧
    29 ∀ i j k : Fin 6, i < j → j < k →
    30 0 < turn (h i) (h j) (h k)
    31
    32/-- A convex hexagon whose convex hull contains no further point of `P`. -/
    33def EmptyConvexHexagon (P : Finset Point) (h : Fin 6 → Point) : Prop :=
    34 StrictConvexHexagon h ∧
    35 (∀ i, h i ∈ P) ∧
    36 ∀ p ∈ P, p ∈ convexHull ℝ (Set.range h) → p ∈ Set.range h
    37
    38/-- The deliberately unoptimized Valtr bound `h(6) ≤ 2^428 + 1`, via 216
    39points in convex position. Its proof in `Lax570090Proofs.EmptyHexagon` uses the
    40four-layer theorem interface, whose proof is also in this package. The
    41visibility-colouring argument uses this interface so Lax records the dependency;
    42the composed proof tree uses only standard logical axioms. -/
    43axiom exists_emptyConvexHexagon
    44 (P : Finset Point) (hP : 2 ^ 428 + 1 ≤ P.card)
    45 (hgeneral : ¬HasThreeCollinear P) :
    46 ∃ h : Fin 6 → Point, EmptyConvexHexagon P h
    47
    48end Lax570090.HujterKisfaludiBak
    49
    Show Proof
    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…