Lax Lean Archive

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

Lax56.HujterKisfaludiBak

The unoptimized empty-hexagon bound

concepts/Lax56/HujterKisfaludiBak.lean · lax-56

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.

    Concept map

    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    Evidence

    Each proof establishes this claim relative to its assumptions.

    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 Lax56Proofs.EmptyHexagonLax56Proofs.EmptyHexagon from Valtr's four-layer lemma. The visibility-colouring theorem is proved in Lax56Proofs.HujterKisfaludiBakLax56Proofs.HujterKisfaludiBak.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Coloring.VertexColoring
    2import Mathlib.Analysis.Convex.Hull
    3import Lax56.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`Lax56Proofs.EmptyHexagon` from Valtr's four-layer lemma. The visibility-colouring
    13theorem is proved in `Lax56Proofs.HujterKisfaludiBak`.
    14-/
    15
    16namespace Lax56.HujterKisfaludiBak
    17
    18open Lax56.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 `Lax56Proofs.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 Lax56.HujterKisfaludiBak
    49
    Show Proof

    Builds on

    Used by

    none

    From Mathlib

    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…