Lax Lean Archive

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

Lax17.PathOfSets

Strong and hairy path-of-sets systems

concepts/Lax17/PathOfSets.lean · lax-17

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

    A path-of-sets system is an ordered sequence of pairwise disjoint connected clusters. Each cluster has equally large, disjoint left and right interfaces, and consecutive interfaces are joined by disjoint path families that otherwise avoid every cluster. It is strong when the two interfaces are well-linked and mutually linked inside each cluster.

    A hairy path-of-sets system adds one disjoint connected hair cluster at every position and a disjoint linkage from the base cluster to that hair. Its hair-side endpoints are well-linked in the hair cluster.

    Lean source view on GitHub

    1import Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
    2import Lax17.Linkedness
    3
    4/-!
    5---
    6title: Strong and hairy path-of-sets systems
    7type: definition
    8---
    9A path-of-sets system is an ordered sequence of pairwise disjoint connected
    10clusters. Each cluster has equally large, disjoint left and right interfaces,
    11and consecutive interfaces are joined by disjoint path families that otherwise
    12avoid every cluster. It is strong when the two interfaces are well-linked and
    13mutually linked inside each cluster.
    14
    15A hairy path-of-sets system adds one disjoint connected hair cluster at every
    16position and a disjoint linkage from the base cluster to that hair. Its
    17hair-side endpoints are well-linked in the hair cluster.
    18-/
    19
    20namespace Lax17.PathOfSets
    21
    22universe u
    23
    24open Lax17.Linkedness
    25open Lax17.Paths
    26
    27/-- A finite vertex set inducing a connected graph. -/
    28def IsCluster {V : Type u} [DecidableEq V]
    29 (G : SimpleGraph V) (C : Finset V) : Prop :=
    30 (G.induce {v : V | v ∈ C}).Connected
    31
    32/-- A path-of-sets system of length `ℓ` and width `w`. -/
    33structure System {V : Type u} [DecidableEq V]
    34 (G : SimpleGraph V) (ℓ w : ℕ) where
    35 length_pos : 0 < ℓ
    36 width_pos : 0 < w
    37 cluster : Fin ℓ → Finset V
    38 cluster_connected : ∀ i : Fin ℓ, IsCluster G (cluster i)
    39 cluster_disjoint :
    40 ∀ ⦃i j : Fin ℓ⦄, i ≠ j → Disjoint (cluster i) (cluster j)
    41 left : Fin ℓ → Finset V
    42 right : Fin ℓ → Finset V
    43 left_subset : ∀ i : Fin ℓ, left i ⊆ cluster i
    44 right_subset : ∀ i : Fin ℓ, right i ⊆ cluster i
    45 interfaces_disjoint : ∀ i : Fin ℓ, Disjoint (left i) (right i)
    46 left_card : ∀ i : Fin ℓ, (left i).card = w
    47 right_card : ∀ i : Fin ℓ, (right i).card = w
    48 connector :
    49 (i : Fin ℓ) → (hi : i.1 + 1 < ℓ) →
    50 VertexLinkage G (right i) (left ⟨i.1 + 1, hi⟩) w
    51 connector_avoids_clusters :
    52 ∀ (i : Fin ℓ) (hi : i.1 + 1 < ℓ) (j : Fin ℓ)
    53 (a : Fin w),
    54 (connector i hi).path a |>.InternallyAvoids (cluster j)
    55 connectors_disjoint :
    56 ∀ ⦃i j : Fin ℓ⦄ (hi : i.1 + 1 < ℓ) (hj : j.1 + 1 < ℓ),
    57 i ≠ j → ∀ a b : Fin w,
    58 Disjoint ((connector i hi).path a).vertices
    59 ((connector j hj).path b).vertices
    60
    61namespace System
    62
    63/-- The first cluster index. -/
    64def firstIndex {V : Type u} [DecidableEq V]
    65 {G : SimpleGraph V} {ℓ w : ℕ}
    66 (P : System G ℓ w) : Fin ℓ :=
    67 ⟨0, P.length_pos⟩
    68
    69/-- The last cluster index. -/
    70def lastIndex {V : Type u} [DecidableEq V]
    71 {G : SimpleGraph V} {ℓ w : ℕ}
    72 (P : System G ℓ w) : Fin ℓ :=
    73 ⟨ℓ - 1, Nat.sub_lt P.length_pos Nat.zero_lt_one⟩
    74
    75end System
    76
    77/-- A strong path-of-sets system. -/
    78structure StrongSystem {V : Type u} [DecidableEq V]
    79 (G : SimpleGraph V) (ℓ w : ℕ) extends System G ℓ w where
    80 left_well_linked :
    81 ∀ i : Fin ℓ, NodeWellLinkedIn G (cluster i) (left i)
    82 right_well_linked :
    83 ∀ i : Fin ℓ, NodeWellLinkedIn G (cluster i) (right i)
    84 interfaces_linked :
    85 ∀ i : Fin ℓ, NodeLinkedIn G (cluster i) (left i) (right i)
    86
    87/-- A hairy path-of-sets system. -/
    88structure HairySystem {V : Type u} [DecidableEq V]
    89 (G : SimpleGraph V) (ℓ w : ℕ) where
    90 base : StrongSystem G ℓ w
    91 hairCluster : Fin ℓ → Finset V
    92 hair_connected : ∀ i : Fin ℓ, IsCluster G (hairCluster i)
    93 hair_disjoint :
    94 ∀ ⦃i j : Fin ℓ⦄, i ≠ j → Disjoint (hairCluster i) (hairCluster j)
    95 hair_disjoint_base :
    96 ∀ i j : Fin ℓ, Disjoint (hairCluster i) (base.cluster j)
    97 hair_disjoint_connectors :
    98 ∀ i j : Fin ℓ, ∀ (hj : j.1 + 1 < ℓ), ∀ a : Fin w,
    99 Disjoint (hairCluster i) ((base.connector j hj).path a).vertices
    100 baseEndpoint : Fin ℓ → Finset V
    101 hairEndpoint : Fin ℓ → Finset V
    102 baseEndpoint_subset :
    103 ∀ i : Fin ℓ, baseEndpoint i ⊆ base.cluster i
    104 hairEndpoint_subset :
    105 ∀ i : Fin ℓ, hairEndpoint i ⊆ hairCluster i
    106 baseEndpoint_card : ∀ i : Fin ℓ, (baseEndpoint i).card = w
    107 hairEndpoint_card : ∀ i : Fin ℓ, (hairEndpoint i).card = w
    108 baseEndpoint_avoids_interfaces :
    109 ∀ i : Fin ℓ,
    110 Disjoint (baseEndpoint i) (base.left i ∪ base.right i)
    111 hairEndpoint_well_linked :
    112 ∀ i : Fin ℓ,
    113 NodeWellLinkedIn G (hairCluster i) (hairEndpoint i)
    114 baseEndpoint_linked :
    115 ∀ i : Fin ℓ,
    116 NodeLinkedIn G (base.cluster i) (base.left i) (baseEndpoint i)
    117 hairLinkage :
    118 ∀ i : Fin ℓ,
    119 VertexLinkage G (baseEndpoint i) (hairEndpoint i) w
    120 hair_linkages_disjoint :
    121 ∀ ⦃i j : Fin ℓ⦄, i ≠ j → ∀ a b : Fin w,
    122 Disjoint ((hairLinkage i).path a).vertices
    123 ((hairLinkage j).path b).vertices
    124 hair_linkages_disjoint_connectors :
    125 ∀ i j : Fin ℓ, ∀ (hj : j.1 + 1 < ℓ), ∀ a b : Fin w,
    126 Disjoint ((hairLinkage i).path a).vertices
    127 ((base.connector j hj).path b).vertices
    128 hair_linkages_avoid_base :
    129 ∀ i j : Fin ℓ, ∀ a : Fin w,
    130 ((hairLinkage i).path a).InternallyAvoids (base.cluster j)
    131 hair_linkages_avoid_hair :
    132 ∀ i j : Fin ℓ, ∀ a : Fin w,
    133 ((hairLinkage i).path a).InternallyAvoids (hairCluster j)
    134
    135/-- The output of splitting one connected cluster into three disjoint
    136connected subclusters while retaining prescribed terminal subsets. -/
    137structure ThreeWayClusterSplit {V : Type u} [DecidableEq V]
    138 (G : SimpleGraph V) (C A B X : Finset V) (q : ℕ) where
    139 firstCluster : Finset V
    140 secondCluster : Finset V
    141 thirdCluster : Finset V
    142 first_subset : firstCluster ⊆ C
    143 second_subset : secondCluster ⊆ C
    144 third_subset : thirdCluster ⊆ C
    145 first_connected : IsCluster G firstCluster
    146 second_connected : IsCluster G secondCluster
    147 third_connected : IsCluster G thirdCluster
    148 first_second_disjoint : Disjoint firstCluster secondCluster
    149 first_third_disjoint : Disjoint firstCluster thirdCluster
    150 second_third_disjoint : Disjoint secondCluster thirdCluster
    151 firstTerminals : Finset V
    152 secondTerminals : Finset V
    153 thirdTerminals : Finset V
    154 firstTerminals_subset :
    155 firstTerminals ⊆ A ∩ firstCluster
    156 secondTerminals_subset :
    157 secondTerminals ⊆ B ∩ secondCluster
    158 thirdTerminals_subset :
    159 thirdTerminals ⊆ X ∩ thirdCluster
    160 first_card : firstTerminals.card = q
    161 second_card : secondTerminals.card = q
    162 third_card : thirdTerminals.card = q
    163 first_well_linked :
    164 NodeWellLinkedIn G firstCluster firstTerminals
    165 second_well_linked :
    166 NodeWellLinkedIn G secondCluster secondTerminals
    167 third_well_linked :
    168 NodeWellLinkedIn G thirdCluster thirdTerminals
    169
    170/-- The Appendix A.3 split of one cluster into a new base cluster and a
    171disjoint hair cluster, together with the retained interfaces and hair
    172linkage. -/
    173structure HairyClusterSplit {V : Type u} [DecidableEq V]
    174 (G : SimpleGraph V) (C A B : Finset V) (w : ℕ) where
    175 baseCluster : Finset V
    176 hairCluster : Finset V
    177 left : Finset V
    178 right : Finset V
    179 baseEndpoint : Finset V
    180 hairEndpoint : Finset V
    181 base_subset : baseCluster ⊆ C
    182 hair_subset : hairCluster ⊆ C
    183 base_connected : IsCluster G baseCluster
    184 hair_connected : IsCluster G hairCluster
    185 clusters_disjoint : Disjoint baseCluster hairCluster
    186 left_subset_base : left ⊆ baseCluster
    187 right_subset_base : right ⊆ baseCluster
    188 baseEndpoint_subset : baseEndpoint ⊆ baseCluster
    189 hairEndpoint_subset : hairEndpoint ⊆ hairCluster
    190 left_subset_original : left ⊆ A
    191 right_subset_original : right ⊆ B
    192 left_card : left.card = w
    193 right_card : right.card = w
    194 baseEndpoint_card : baseEndpoint.card = w
    195 hairEndpoint_card : hairEndpoint.card = w
    196 interfaces_disjoint : Disjoint left right
    197 baseEndpoint_disjoint_interfaces :
    198 Disjoint baseEndpoint (left ∪ right)
    199 left_well_linked : NodeWellLinkedIn G baseCluster left
    200 right_well_linked : NodeWellLinkedIn G baseCluster right
    201 interfaces_linked : NodeLinkedIn G baseCluster left right
    202 left_baseEndpoint_linked :
    203 NodeLinkedIn G baseCluster left baseEndpoint
    204 hairEndpoint_well_linked :
    205 NodeWellLinkedIn G hairCluster hairEndpoint
    206 hairLinkage :
    207 VertexLinkage G baseEndpoint hairEndpoint w
    208 hairLinkage_stays_in_cluster :
    209 ∀ i : Fin w, (hairLinkage.path i).StaysIn C
    210 hairLinkage_avoids_base :
    211 ∀ i : Fin w, (hairLinkage.path i).InternallyAvoids baseCluster
    212 hairLinkage_avoids_hair :
    213 ∀ i : Fin w, (hairLinkage.path i).InternallyAvoids hairCluster
    214
    215end Lax17.PathOfSets
    216

    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…