Lax Lean Archive

Many atomic types force atomically matched tuples

Lax185574.MatchedTuples · concepts/Lax185574/MatchedTuples.lean · lax-185574

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

    Theorem

    There exists a computable function Q : ℕ → ℕ such that for every ℓ ∈ ℕ and for every bipartite graph G = (L, R, E) with |ATypes(L/R)| > Q(ℓ), there are two tuples ā ∈ L^ℓ and b̄ ∈ R^ℓ that are atomically matched in G.

    This is Corollary 2.4 of Ding, Oporowski, Oxley and Vertigan (1996), see also Theorem 2 of Gravier, Maffray, Renault and Trotignon (2004).

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

    Each proof establishes this claim relative to its assumptions.

    In the paper

    • page 22 of this submission's paper

    Lean source view on GitHub

    1import Lax185574.AtomicMatching
    2import Lax185574.AtomicTypes
    3import Lax185574.BipartiteGraphs
    4import Mathlib.Computability.Partrec
    5
    6/-!
    7---
    8title: Many atomic types force atomically matched tuples
    9type: theorem
    10---
    11There exists a computable function Q : ℕ → ℕ such that for every ℓ ∈ ℕ
    12and for every bipartite graph G = (L, R, E) with |ATypes(L/R)| > Q(ℓ),
    13there are two tuples ā ∈ L^ℓ and b̄ ∈ R^ℓ that are atomically matched
    14in G.
    15
    16This is Corollary 2.4 of Ding, Oporowski, Oxley and Vertigan (1996), see
    17also Theorem 2 of Gravier, Maffray, Renault and Trotignon (2004).
    18
    19# Formalization notes
    20
    21A bipartite graph (L, R, E) is given by two finite types L and R and a
    22relation E between them. Its graph is the simple graph on L ⊕ R whose
    23edges are the pairs related by E, `BipartiteGraphs.bipartiteGraph E`. The number
    24|ATypes(L/R)| is `AtomicTypes.atomicTypeCount` of this graph, for the
    25vertices of L over the vertices of R. Since L and R are disjoint, it is
    26the number of distinct neighborhoods of vertices of L. Computability of
    27Q is mathlib's `Computable`. The two sides are finite, which covers the
    28use in the paper inside the proof of the ball-types lemma.
    29-/
    30
    31namespace Lax185574.MatchedTuples
    32
    33open Lax185574.AtomicMatching Lax185574.AtomicTypes Lax185574.BipartiteGraphs
    34
    35universe u v
    36
    37/-- **Matchings, co-matchings and half-graphs.** A computable `Q` such
    38that a bipartite graph whose left side realizes more than `Q(ℓ)` atomic
    39types over the right side contains atomically matched `ℓ`-tuples, one
    40from each side. -/
    41axiom exists_atomicallyMatched :
    42 ∃ Q : ℕ → ℕ, Computable Q ∧
    43 ∀ (ℓ : ℕ) (L : Type u) (R : Type v) [Finite L] [Finite R] (E : L → R → Prop),
    44 Q ℓ < atomicTypeCount (bipartiteGraph E) (Set.range Sum.inl)
    45 (Set.range Sum.inr) →
    46 ∃ (a : Fin ℓ → L) (b : Fin ℓ → R),
    47 AtomicallyMatched (bipartiteGraph E) (Sum.inl ∘ a) (Sum.inr ∘ b)
    48
    49end Lax185574.MatchedTuples
    50
    Show Proof
    Formalization notes

    A bipartite graph (L, R, E) is given by two finite types L and R and a relation E between them. Its graph is the simple graph on L ⊕ R whose edges are the pairs related by E, BipartiteGraphs.bipartiteGraphEBipartiteGraphs.bipartiteGraph E. The number |ATypes(L/R)| is AtomicTypes.atomicTypeCountAtomicTypes.atomicTypeCount of this graph, for the vertices of L over the vertices of R. Since L and R are disjoint, it is the number of distinct neighborhoods of vertices of L. Computability of Q is mathlib's ComputableComputable. The two sides are finite, which covers the use in the paper inside the proof of the ball-types lemma.

    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…