Lax Lean Archive

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

Matching occurrences and raw unit types

Lax342547.MatchingSamples · concepts/Lax342547/MatchingSamples.lean · lax-342547

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

    Every touching matching has an injective orientation on sample positions. Its raw unit types form an independent conflict set even when different matching edges have identical raw types.

    Concept map
    3 concepts; 9 descendants hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 7 statements. Each proof establishes one of them relative to its assumptions.

    1 matching_orientation_injective proven

    2 matching_unit_independence proven

    3 matching_unit_is_unit proven

    4 oriented_covers proven

    5 oriented_injective proven

    6 oriented_mem proven

    7 unit_types_independent proven

    Lean source view on GitHub

    1import Lax342547.SampledGraph
    2import Lax342547.ConnectedMatching
    3import Mathlib.Data.Fintype.EquivFin
    4
    5/-!
    6---
    7title: Matching occurrences and raw unit types
    8type: lemma
    9---
    10Every touching matching has an injective orientation on sample positions. Its raw unit types form an independent conflict set even when different matching edges have identical raw types.
    11-/
    12
    13namespace Lax342547.MatchingSamples
    14
    15open Lax342547.ConnectedMatching Lax342547.SampledGraph
    16
    17noncomputable def oriented {V : Type} (e : Finset V) (he : e.card = 2) : Bool → V :=
    18 fun b => ((e.equivFinOfCardEq he).symm (if b then 1 else 0)).val
    19
    20axiom oriented_mem {V : Type} (e : Finset V) (he : e.card = 2) (b : Bool) : oriented e he b ∈ e
    21
    22axiom oriented_injective {V : Type} (e : Finset V) (he : e.card = 2) : Function.Injective (oriented e he)
    23
    24axiom oriented_covers {V : Type} (e : Finset V) (he : e.card = 2) (v : V) (hv : v ∈ e) :
    25 ∃ b, oriented e he b = v
    26
    27axiom matching_orientation_injective {V : Type} (G : SimpleGraph V) (M : Finset (Finset V))
    28 (hM : IsTouchingMatching G M) :
    29 Function.Injective (fun eb : M × Bool => oriented eb.1.val (hM.1 _ eb.1.property).1 eb.2)
    30
    31axiom matching_unit_independence {Ω : Type} (hole : Ω → Ω → Prop)
    32 (hsymm : ∀ ⦃x y⦄, hole x y → hole y x) (hloop : ∀ x, ¬ hole x x)
    33 {m : ℕ} (sample : Fin m → Ω) (M : Finset (Finset (Fin m)))
    34 (hM : IsTouchingMatching (sampleGraph hole hsymm sample) M) :
    35 ∀ e f : M, ¬ (∀ i j : Bool,
    36 hole (sample (oriented e.val (hM.1 _ e.property).1 i))
    37 (sample (oriented f.val (hM.1 _ f.property).1 j)))
    38
    39noncomputable def unitType {Ω : Type} {m : ℕ} (sample : Fin m → Ω)
    40 (e : Finset (Fin m)) (he : e.card = 2) : Ω × Ω :=
    41 (sample (oriented e he false),sample (oriented e he true))
    42
    43def fourConflict {Ω : Type} (hole : Ω → Ω → Prop) (u v : Ω × Ω) : Prop :=
    44 hole u.1 v.1 ∧ hole u.1 v.2 ∧ hole u.2 v.1 ∧ hole u.2 v.2
    45
    46axiom matching_unit_is_unit {Ω : Type} (hole : Ω → Ω → Prop)
    47 (hsymm : ∀ ⦃x y⦄, hole x y → hole y x)
    48 {m : ℕ} (sample : Fin m → Ω) (M : Finset (Finset (Fin m)))
    49 (hM : IsTouchingMatching (sampleGraph hole hsymm sample) M) (e : M) :
    50 ¬ hole (unitType sample e.val (hM.1 _ e.property).1).1
    51 (unitType sample e.val (hM.1 _ e.property).1).2
    52
    53axiom unit_types_independent {Ω : Type} (hole : Ω → Ω → Prop)
    54 (hsymm : ∀ ⦃x y⦄, hole x y → hole y x) (hloop : ∀ x, ¬ hole x x)
    55 {m : ℕ} (sample : Fin m → Ω) (M : Finset (Finset (Fin m)))
    56 (hM : IsTouchingMatching (sampleGraph hole hsymm sample) M) : by
    57 classical
    58 exact let I := Finset.univ.image (fun e : M => unitType sample e.val (hM.1 _ e.property).1)
    59 (∀ u ∈ I, ¬ hole u.1 u.2) ∧ (∀ u ∈ I, ∀ v ∈ I, ¬ fourConflict hole u v)
    60
    61end Lax342547.MatchingSamples
    62
    Show ProofShow ProofShow ProofShow ProofShow ProofShow ProofShow Proof
    Builds on
    Used by
    From Mathlib

    Discussion

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

    Loading discussion…