Documentation

Complexitylib.Algebraic.LowerBound.Cutwidth.MedianOrdering

Ordering a cubic graph by median edge positions #

Given a path decomposition of a simple 3-regular graph, place every edge at a position inside a bag containing its endpoints, so that positions are distinct and increase with the bag index. Each vertex has three incident positions; order the vertices by the middle one. Then every prefix cut has at most one more edge than the bag in which the last vertex's median edge lies: a crossing edge below the median of the last vertex is the unique low edge of its later endpoint, one above it is the unique high edge of its earlier endpoint, and the median itself is a single edge. Each charged vertex lies in that bag by consecutiveness.

The main result is card_cutFinset_key_lt_le: with bags of size at most p + 1, an injective key orders the vertices so that every prefix cut has at most p + 2 edges.

Bags indexed by natural numbers #

source
noncomputable def Algebraic.Cutwidth.MedianOrdering.bagN {W : Type} (H : SimpleGraph W) (D : PathDecomposition H) (i : ℕ) :
Finset W

The bag with index i, or the empty set beyond the decomposition.

Equations
Instances For
    source
    theorem Algebraic.Cutwidth.MedianOrdering.card_bagN_le {W : Type} (H : SimpleGraph W) (D : PathDecomposition H) {p : ℕ} (hbag : ∀ (i : Fin D.length), (D.bag i).card ≤ p + 1) (i : ℕ) :
    (bagN H D i).card ≤ p + 1
    source
    theorem Algebraic.Cutwidth.MedianOrdering.bagN_consecutive {W : Type} (H : SimpleGraph W) (D : PathDecomposition H) {w : W} {i j k : ℕ} (hij : i ≤ j) (hjk : j ≤ k) (hi : w ∈ bagN H D i) (hk : w ∈ bagN H D k) :
    w ∈ bagN H D j
    source
    noncomputable def Algebraic.Cutwidth.MedianOrdering.bagOf {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (D : PathDecomposition H) (e : Sym2 W) :
    ℕ

    A bag containing both endpoints of an edge; 0 for non-edges.

    Equations
    Instances For
      source
      theorem Algebraic.Cutwidth.MedianOrdering.mem_bagN_bagOf {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (D : PathDecomposition H) {e : Sym2 W} (he : e ∈ H.edgeSet) {a : W} (ha : a ∈ e) :
      a ∈ bagN H D (bagOf H D e)

      Edge positions #

      source
      noncomputable def Algebraic.Cutwidth.MedianOrdering.rank {W : Type} [Fintype W] (e : Sym2 W) :
      ℕ

      An injective rank of the edges.

      Equations
      Instances For
        source
        theorem Algebraic.Cutwidth.MedianOrdering.rank_lt {W : Type} [Fintype W] (e : Sym2 W) :
        rank e < Fintype.card (Sym2 W)
        source
        theorem Algebraic.Cutwidth.MedianOrdering.rank_injective {W : Type} [Fintype W] :
        Function.Injective rank
        source
        noncomputable def Algebraic.Cutwidth.MedianOrdering.pos {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (D : PathDecomposition H) (e : Sym2 W) :
        ℕ

        The position of an edge: its bag index, refined by its rank.

        Equations
        Instances For
          source
          theorem Algebraic.Cutwidth.MedianOrdering.digit_le_of_le {b b' r r' c : ℕ} (hr' : r' < c) (h : b * c + r ≤ b' * c + r') :
          b ≤ b'

          Mixed-radix comparison: the leading digit is monotone.

          source
          theorem Algebraic.Cutwidth.MedianOrdering.pos_injective {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (D : PathDecomposition H) :
          Function.Injective (pos H D)
          source
          theorem Algebraic.Cutwidth.MedianOrdering.bagOf_le_of_pos_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) (D : PathDecomposition H) {e e' : Sym2 W} (h : pos H D e ≤ pos H D e') :
          bagOf H D e ≤ bagOf H D e'

          Incident edges and medians #

          source
          theorem Algebraic.Cutwidth.MedianOrdering.mem_incidenceFinset_iff {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] {u : W} {e : Sym2 W} :
          e ∈ H.incidenceFinset u ↔ e ∈ H.edgeSet ∧ u ∈ e
          source
          theorem Algebraic.Cutwidth.MedianOrdering.card_incidenceFinset {W : Type} [Fintype W] (H : SimpleGraph W) [DecidableRel H.Adj] (regular : H.IsRegularOfDegree 3) (u : W) :
          (H.incidenceFinset u).card = 3
          source
          theorem Algebraic.Cutwidth.MedianOrdering.exists_median {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
          ∃ e ∈ H.incidenceFinset u, (∃ e₁ ∈ H.incidenceFinset u, pos H D e₁ < pos H D e) ∧ ∃ e₂ ∈ H.incidenceFinset u, pos H D e < pos H D e₂

          Among the three incident edges of a vertex there is a middle one.

          source
          noncomputable def Algebraic.Cutwidth.MedianOrdering.median {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
          Sym2 W

          The median edge of a vertex.

          Equations
          Instances For
            source
            theorem Algebraic.Cutwidth.MedianOrdering.median_mem {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
            median H D regular u ∈ H.incidenceFinset u
            source
            theorem Algebraic.Cutwidth.MedianOrdering.exists_lt_median {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
            ∃ e₁ ∈ H.incidenceFinset u, pos H D e₁ < pos H D (median H D regular u)
            source
            theorem Algebraic.Cutwidth.MedianOrdering.exists_median_lt {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
            ∃ e₂ ∈ H.incidenceFinset u, pos H D (median H D regular u) < pos H D e₂
            source
            noncomputable def Algebraic.Cutwidth.MedianOrdering.theta {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
            ℕ

            The position of the median edge.

            Equations
            Instances For
              source
              theorem Algebraic.Cutwidth.MedianOrdering.incidenceFinset_eq {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
              H.incidenceFinset u = {e ∈ H.incidenceFinset u | pos H D e < theta H D regular u} ∪ {e ∈ H.incidenceFinset u | theta H D regular u < pos H D e} ∪ {median H D regular u}

              The incident edges split into those below, at, and above the median.

              source
              theorem Algebraic.Cutwidth.MedianOrdering.card_below_add_card_above {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (u : W) :
              {e ∈ H.incidenceFinset u | pos H D e < theta H D regular u}.card + {e ∈ H.incidenceFinset u | theta H D regular u < pos H D e}.card + 1 = 3
              source
              theorem Algebraic.Cutwidth.MedianOrdering.eq_of_lt_theta {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) {u : W} {e e' : Sym2 W} (he : e ∈ H.incidenceFinset u) (he' : e' ∈ H.incidenceFinset u) (h : pos H D e < theta H D regular u) (h' : pos H D e' < theta H D regular u) :
              e = e'

              At most one incident edge lies below the median.

              source
              theorem Algebraic.Cutwidth.MedianOrdering.eq_of_theta_lt {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) {u : W} {e e' : Sym2 W} (he : e ∈ H.incidenceFinset u) (he' : e' ∈ H.incidenceFinset u) (h : theta H D regular u < pos H D e) (h' : theta H D regular u < pos H D e') :
              e = e'

              At most one incident edge lies above the median.

              The vertex ordering #

              source
              noncomputable def Algebraic.Cutwidth.MedianOrdering.key {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) (w : W) :
              ℕ

              The ordering key of a vertex: its median position, refined by a rank.

              Equations
              Instances For
                source
                theorem Algebraic.Cutwidth.MedianOrdering.key_injective {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) :
                Function.Injective (key H D regular)
                source
                theorem Algebraic.Cutwidth.MedianOrdering.theta_le_of_key_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) {w w' : W} (h : key H D regular w ≤ key H D regular w') :
                theta H D regular w ≤ theta H D regular w'
                source
                theorem Algebraic.Cutwidth.MedianOrdering.card_cutFinset_key_lt_le {W : Type} [Fintype W] [DecidableEq W] (H : SimpleGraph W) [DecidableRel H.Adj] (D : PathDecomposition H) (regular : H.IsRegularOfDegree 3) {p : ℕ} (hbag : ∀ (i : Fin D.length), (D.bag i).card ≤ p + 1) (t : ℕ) :
                (H.cutFinset {w : W | key H D regular w < t}).card ≤ p + 2

                The median ordering bound. Every prefix of the key ordering has a cut of at most p + 2 edges when all bags have at most p + 1 vertices.