Lax Lean Archive

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

Lax17.Crossbar

Crossbars and pseudo-grids

concepts/Lax17/Crossbar.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

    An (A,B,X)(A,B,X)-crossbar consists of disjoint main paths from AA to BB and one disjoint spoke from every main path to XX. Each spoke meets its own main path exactly once and avoids all other main paths.

    A pseudo-grid records the alternative produced by Theorem 4.1: disjoint AA-to-BB rows, disjoint selected columns reaching XX, and disjoint small blocks of rows. Property P1 says that every unreserved row avoids all selected columns; property P2 says that, for each reserved block, all but at most 2g22g^2 columns meet a row in that block.

    Lean source view on GitHub

    1import Lax17.Minor
    2import Lax17.PathOfSets
    3import Lax17.Paths
    4
    5/-!
    6---
    7title: Crossbars and pseudo-grids
    8type: definition
    9---
    10An \((A,B,X)\)-crossbar consists of disjoint main paths from \(A\) to \(B\)
    11and one disjoint spoke from every main path to \(X\). Each spoke meets its own
    12main path exactly once and avoids all other main paths.
    13
    14A pseudo-grid records the alternative produced by Theorem 4.1: disjoint
    15\(A\)-to-\(B\) rows, disjoint selected columns reaching \(X\), and disjoint
    16small blocks of rows. Property P1 says that every unreserved row avoids all
    17selected columns; property P2 says that, for each reserved block, all but at
    18most \(2g^2\) columns meet a row in that block.
    19-/
    20
    21namespace Lax17.Crossbar
    22
    23universe u
    24
    25open Lax17.Paths
    26
    27/-- The parameter is an integral power of two. -/
    28def IsPowerOfTwo (g : ℕ) : Prop :=
    29 ∃ exponent : ℕ, g = 2 ^ exponent
    30
    31/-- The graph has a minor carrying a strong path-of-sets system of the
    32specified length and width. -/
    33def HasStrongPathOfSetsMinor {V : Type u} [DecidableEq V]
    34 (G : SimpleGraph V) (length width : ℕ) : Prop :=
    35 ∃ (W : Type u) (_ : Fintype W) (_ : DecidableEq W)
    36 (H : SimpleGraph W),
    37 Lax17.Minor.IsMinor H G ∧
    38 Nonempty (Lax17.PathOfSets.StrongSystem H length width)
    39
    40/-- A crossbar of width `ρ`. -/
    41structure System {V : Type u} [DecidableEq V]
    42 (G : SimpleGraph V) (A B X : Finset V) (ρ : ℕ) where
    43 mainPath : Fin ρ → Path G
    44 main_connects : ∀ i : Fin ρ, (mainPath i).Connects A B
    45 main_disjoint :
    46 Pairwise fun i j => Disjoint (mainPath i).vertices (mainPath j).vertices
    47 spokePath : Fin ρ → Path G
    48 spoke_disjoint :
    49 Pairwise fun i j => Disjoint (spokePath i).vertices (spokePath j).vertices
    50 attachment : Fin ρ → V
    51 attachment_on_main :
    52 ∀ i : Fin ρ, attachment i ∈ (mainPath i).vertices
    53 attachment_on_spoke :
    54 ∀ i : Fin ρ, attachment i ∈ (spokePath i).vertices
    55 exact_attachment :
    56 ∀ i : Fin ρ,
    57 (mainPath i).vertices ∩ (spokePath i).vertices = {attachment i}
    58 exit : Fin ρ → V
    59 attachment_is_endpoint :
    60 ∀ i : Fin ρ,
    61 attachment i = (spokePath i).source ∨
    62 attachment i = (spokePath i).target
    63 exit_is_other_endpoint :
    64 ∀ i : Fin ρ,
    65 exit i =
    66 if (spokePath i).source = attachment i then
    67 (spokePath i).target
    68 else
    69 (spokePath i).source
    70 exit_in_X : ∀ i : Fin ρ, exit i ∈ X
    71 exit_off_main :
    72 ∀ i : Fin ρ, exit i ∉ (mainPath i).vertices
    73 spoke_avoids_other_main :
    74 ∀ ⦃i j : Fin ρ⦄, i ≠ j →
    75 Disjoint (spokePath i).vertices (mainPath j).vertices
    76
    77/-- A depth-`D` pseudo-grid with `κ` main rows at scale `g`. -/
    78structure PseudoGrid {V : Type u} [DecidableEq V]
    79 (G : SimpleGraph V) (A B X : Finset V)
    80 (g D κ : ℕ) where
    81 RowIndex : Type
    82 [rowFintype : Fintype RowIndex]
    83 [rowDecidableEq : DecidableEq RowIndex]
    84 row_count : Fintype.card RowIndex = κ
    85 row : RowIndex → Path G
    86 row_connects : ∀ i : RowIndex, (row i).Connects A B
    87 rows_disjoint :
    88 Pairwise fun i j => Disjoint (row i).vertices (row j).vertices
    89 depth_pos : 0 < D
    90 reserved : Fin D → Finset RowIndex
    91 reserved_card_le :
    92 ∀ i : Fin D, (reserved i).card ≤ g ^ 2
    93 reserved_disjoint :
    94 ∀ ⦃i j : Fin D⦄, i ≠ j →
    95 Disjoint (reserved i) (reserved j)
    96 ColumnIndex : Type
    97 [columnFintype : Fintype ColumnIndex]
    98 [columnDecidableEq : DecidableEq ColumnIndex]
    99 column_count : Fintype.card ColumnIndex = κ / 4
    100 column : ColumnIndex → Path G
    101 columns_disjoint :
    102 Pairwise fun i j => Disjoint (column i).vertices (column j).vertices
    103 column_reaches_X_cleanly :
    104 ∀ j : ColumnIndex,
    105 ((column j).source ∈ X ∨ (column j).target ∈ X) ∧
    106 (column j).InternallyAvoids X
    107 unreserved_row_avoids_columns :
    108 ∀ p : RowIndex,
    109 (∀ i : Fin D, p ∉ reserved i) →
    110 ∀ j : ColumnIndex,
    111 Disjoint (row p).vertices (column j).vertices
    112 few_columns_miss_reserved :
    113 ∀ i : Fin D,
    114 ∃ miss : Finset ColumnIndex,
    115 miss.card ≤ 2 * g ^ 2 ∧
    116 ∀ j : ColumnIndex, j ∉ miss →
    117 ∃ p ∈ reserved i,
    118 ¬ Disjoint (row p).vertices (column j).vertices
    119
    120end Lax17.Crossbar
    121

    Builds on

    Used by

    From Mathlib

    none

    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…