Lax Lean Archive

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

Lax56.ConvexLayers

Convex layers and minimal polygons

concepts/Lax56/ConvexLayers.lean · lax-56

definition

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

    Definition

    The unordered, finite-set definitions used in the unoptimized convex-layer route to Valtr's empty-hexagon theorem. No geometric theorem is assumed here.

    Lean source view on GitHub

    1import Lax56.Geometry
    2import Mathlib.Analysis.Convex.Independent
    3
    4/-!
    5---
    6title: Convex layers and minimal polygons
    7type: definition
    8---
    9The unordered, finite-set definitions used in the unoptimized convex-layer
    10route to Valtr's empty-hexagon theorem. No geometric theorem is assumed here.
    11-/
    12
    13namespace Lax56.ConvexLayers
    14
    15open Lax56.Geometry
    16open scoped Classical
    17
    18/-- Every point is a vertex: no point lies in the convex hull of the others. -/
    19def ConvexPosition (P : Finset Point) : Prop :=
    20 ConvexIndependent ℝ (fun p : {p : Point // p ∈ P} ↦ p.val)
    21
    22/-- Vertices of the convex hull, including all points of sets of size at most two. -/
    23noncomputable def extremeLayer (P : Finset Point) : Finset Point :=
    24 P.filter (fun p ↦ p ∈ (convexHull ℝ (P : Set Point)).extremePoints ℝ)
    25
    26/-- The remainder after deleting the current outer layer. -/
    27noncomputable def inner (P : Finset Point) : Finset Point := P \ extremeLayer P
    28
    29/-- The remainder after `n` layers have been removed. -/
    30noncomputable def remainder (P : Finset Point) : ℕ → Finset Point
    31 | 0 => P
    32 | n + 1 => inner (remainder P n)
    33
    34/-- Layers are indexed from zero: `layer P 0` is the outer layer. -/
    35noncomputable def layer (P : Finset Point) (n : ℕ) : Finset Point :=
    36 extremeLayer (remainder P n)
    37
    38/-- All ambient points in the convex hull of `A`, not just its interior points. -/
    39noncomputable def hullClosure (P A : Finset Point) : Finset Point :=
    40 P.filter (fun p ↦ p ∈ convexHull ℝ (A : Set Point))
    41
    42/-- Passing from `P` to `S` loses no ambient point inside the new convex hull. -/
    43def HullClosedIn (P S : Finset Point) : Prop :=
    44 S ⊆ P ∧ ∀ p ∈ P, p ∈ convexHull ℝ (S : Set Point) → p ∈ S
    45
    46/-- The exact minimality condition in the proposed four-layer lemma. -/
    47def MinimalOuter (S : Finset Point) : Prop :=
    48 ∀ X ⊆ S, ConvexPosition X → (extremeLayer S).card ≤ X.card → X = extremeLayer S
    49
    50/-- An unordered empty convex polygon with exactly `k` vertices. -/
    51def EmptyPolygon (P H : Finset Point) (k : ℕ) : Prop :=
    52 H ⊆ P ∧ H.card = k ∧ ConvexPosition H ∧
    53 ∀ p ∈ P, p ∈ convexHull ℝ (H : Set Point) → p ∈ H
    54
    55def HasEmptyHexagon (P : Finset Point) : Prop :=
    56 ∃ H, EmptyPolygon P H 6
    57
    58end Lax56.ConvexLayers
    59

    Builds on

    Used by

    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…