Lax Lean Archive

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

The Matching Number of a Bipartite Graph in Time O(n · |x|)

Lax117284.BipartiteKuhnTime · concepts/Lax117284/BipartiteKuhnTime.lean · lax-117284

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 is one word RAM program and one constant cc such that, at every word length ww, given a bipartite graph split at nn as a word xx with c (∣x∣+1)≤2wc\,(|x|+1) \le 2^w, the program halts within c (n+1) (∣x∣+1)c\,(n+1)\,(|x|+1) instructions with the matching number of the graph as its single output entry. Since the word has length 3+V+2E+13 + V + 2E + 1 for VV vertices and EE edges, this is Kuhn's bound O(∣L∣⋅(∣V∣+∣E∣))O(|L| \cdot (|V| + |E|)), hence O(∣V∣⋅∣E∣)O(|V| \cdot |E|) on graphs without isolated vertices.

    Concept map
    6 concepts; 1 descendant hidden
    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 Lax117284.BipartiteGraph
    2import Lax117284.BipartiteMatching
    3import Lax808846.RamComputes
    4
    5/-!
    6---
    7title: The Matching Number of a Bipartite Graph in Time O(n · |x|)
    8type: theorem
    9---
    10There is one word RAM program and one constant cc such that, at every word length ww, given a
    11bipartite graph split at nn as a word xx with c (∣x∣+1)≤2wc\,(|x|+1) \le 2^w, the program halts within
    12c (n+1) (∣x∣+1)c\,(n+1)\,(|x|+1) instructions with the matching number of the graph as its single output
    13entry. Since the word has length 3+V+2E+13 + V + 2E + 1 for VV vertices and EE edges, this is Kuhn's
    14bound O(∣L∣⋅(∣V∣+∣E∣))O(|L| \cdot (|V| + |E|)), hence O(∣V∣⋅∣E∣)O(|V| \cdot |E|) on graphs without isolated vertices.
    15
    16# Formalization Notes
    17
    18The program runs one augmenting search per left vertex, in the order of the word. A search
    19marks each right vertex at most once, scans the adjacency list of each left vertex it reaches at
    20most once, and clears its marks before the next search; so a search costs a number of
    21instructions linear in the length of the word, and the nn searches cost c n (∣x∣+1)c\,n\,(|x|+1). The
    22matching itself is left in memory; the output is its size, which is a function of the graph
    23alone, whereas which maximum matching is found depends on the order of the lists.
    24
    25The admissible inputs are the encodings of bipartite graphs split at their last entry that fit
    26the word length. Every value the program manipulates — a vertex, an offset into the word, a
    27counter, a step count — is below c (∣x∣+1)c\,(|x|+1), so the one fitting condition on the word suffices.
    28The program is quantified before the word length: it is one algorithm, uniform in ww.
    29-/
    30
    31namespace Lax117284.BipartiteKuhnTime
    32
    33open Lax808846.Ram Lax808846.RamComputes Lax117284.BipartiteGraph Lax117284.BipartiteMatching
    34
    35open scoped Classical in
    36/-- **The matching number is computed within `c · (n + 1) · (|x| + 1)` instructions** by one
    37word RAM program at every word length that fits the word. -/
    38axiom computes : ∃ (prog : Program) (c : ℕ), ∀ w : ℕ,
    39 ComputesInTime w prog
    40 {x | (∃ (V : ℕ) (G : SimpleGraph (Fin V)) (n : ℕ), EncodesBipartite x V G n) ∧
    41 c * (x.length + 1) ≤ 2 ^ w}
    42 (fun x => [matchingNumber (wordGraph x)])
    43 (fun x => c * (leftCount x + 1) * (x.length + 1))
    44
    45end Lax117284.BipartiteKuhnTime
    46
    Show Proof
    Formalization Notes

    The program runs one augmenting search per left vertex, in the order of the word. A search marks each right vertex at most once, scans the adjacency list of each left vertex it reaches at most once, and clears its marks before the next search; so a search costs a number of instructions linear in the length of the word, and the nn searches cost c n (∣x∣+1)c\,n\,(|x|+1). The matching itself is left in memory; the output is its size, which is a function of the graph alone, whereas which maximum matching is found depends on the order of the lists.

    The admissible inputs are the encodings of bipartite graphs split at their last entry that fit the word length. Every value the program manipulates — a vertex, an offset into the word, a counter, a step count — is below c (∣x∣+1)c\,(|x|+1), so the one fitting condition on the word suffices. The program is quantified before the word length: it is one algorithm, uniform in ww.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…