Lax Lean Archive

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

The Gossiping Problem

Lax630294.Gossiping · concepts/Lax630294/Gossiping.lean · lax-630294

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.

    Natural Language Statement

    Definition

    Let GG be a multigraph. A labeling assigns a natural number to every edge. A strict temporal path from uu to vv is a path from uu to vv in GG whose edge labels strictly increase in traversal order; the path of length zero is allowed. The labeled graph is temporally connected if, for every ordered pair of vertices u,vu, v, there is a strict temporal path from uu to vv. The instance GG of Gossiping is a yes-instance if some labeling makes GG temporally connected.

    Interpreting each edge as a call between its endpoints and each label as the time of the call, a labeling is an ordering of the calls, and it is temporally connected exactly when every participant learns every secret.

    Concept map
    1 concept; 1 descendant hidden
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A

    In the paper

    • page 2 of this submission's paper
    • page 3 of this submission's paper

    Lean source view on GitHub

    1import Mathlib.Combinatorics.Graph.Basic
    2import Mathlib.Order.Fin.Basic
    3import Mathlib.Order.Monotone.Basic
    4
    5/-!
    6---
    7title: The Gossiping Problem
    8type: definition
    9---
    10
    11Let `G` be a multigraph. A *labeling* assigns a natural number to every edge.
    12A *strict temporal path* from `u` to `v` is a path from `u` to `v` in `G` whose
    13edge labels strictly increase in traversal order; the path of length zero is
    14allowed. The labeled graph is *temporally connected* if, for every ordered pair
    15of vertices `u, v`, there is a strict temporal path from `u` to `v`. The instance
    16`G` of Gossiping is a *yes-instance* if some labeling makes `G` temporally
    17connected.
    18
    19Interpreting each edge as a call between its endpoints and each label as the
    20time of the call, a labeling is an ordering of the calls, and it is temporally
    21connected exactly when every participant learns every secret.
    22
    23# Formalization notes
    24
    25Multigraphs are Mathlib's `Graph α β`, with vertex type `α` and edge type `β`;
    26parallel edges and loops are allowed, and `G.IsLink e x y` states that the edge
    27`e` has the ends `x` and `y`. Finiteness is not part of the definition and is
    28assumed where it matters. Loops never lie on a path, so they do not influence
    29the answer. Labels are taken in `ℕ`; only their relative order matters. A path
    30of length `k` is given by its `k + 1` pairwise distinct vertices `x 0, …, x k`
    31and its `k` edges `e 0, …, e (k - 1)`, where `e i` links `x i` and `x (i + 1)`.
    32A graph with at most one vertex is a yes-instance, since only paths of length
    33zero are required.
    34-/
    35
    36namespace Lax630294.Gossiping
    37
    38open Graph
    39
    40variable {α β : Type*}
    41
    42/-- A strict temporal path from `u` to `v` with respect to the labeling `ℓ`: a path
    43of some length `k` whose edge labels strictly increase along the path. -/
    44def HasTemporalPath (G : Graph α β) (ℓ : β → ℕ) (u v : α) : Prop :=
    45 ∃ (k : ℕ) (x : Fin (k + 1) → α) (e : Fin k → β),
    46 x 0 = u ∧ x (Fin.last k) = v ∧ Function.Injective x ∧
    47 (∀ i : Fin k, G.IsLink (e i) (x i.castSucc) (x i.succ)) ∧
    48 StrictMono (fun i => ℓ (e i))
    49
    50/-- The labeling `ℓ` makes `G` temporally connected: every vertex reaches every
    51vertex by a strict temporal path. -/
    52def IsTemporallyConnected (G : Graph α β) (ℓ : β → ℕ) : Prop :=
    53 ∀ u ∈ V(G), ∀ v ∈ V(G), HasTemporalPath G ℓ u v
    54
    55/-- `G` is label-connected, i.e. a yes-instance of Gossiping: some labeling makes it temporally connected. -/
    56def IsLabelConnected (G : Graph α β) : Prop :=
    57 ∃ ℓ : β → ℕ, IsTemporallyConnected G ℓ
    58
    59end Lax630294.Gossiping
    60
    Formalization notes

    Multigraphs are Mathlib's GraphαβGraph α β, with vertex type αα and edge type ββ; parallel edges and loops are allowed, and G.IsLinkexyG.IsLink e x y states that the edge ee has the ends xx and yy. Finiteness is not part of the definition and is assumed where it matters. Loops never lie on a path, so they do not influence the answer. Labels are taken in Nℕ; only their relative order matters. A path of length kk is given by its k+1k + 1 pairwise distinct vertices x0,…,xkx 0, …, x k and its kk edges e0,…,e(k−1)e 0, …, e (k - 1), where eie i links xix i and x(i+1)x (i + 1). A graph with at most one vertex is a yes-instance, since only paths of length zero are required.

    Builds on

    none

    Used by
    From Mathlib

    Discussion

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

    Loading discussion…