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

Gossiping and the Characterization by T-Graphs and M-Graphs

lax-630294·formalized by Ralf Klasing · George B. Mertzios · Hendrik Molter @hendrikmolter · Nils Morawietz · Paul G. Spirakis · Claude Code·created ·GitHub @d280f8e·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Sign in with ORCID

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    In the Gossiping problem, the edges of a multigraph GG are calls between participants, and one asks for an ordering of the calls, given by a labeling of the edges with natural numbers, such that every participant learns the secret of every other participant. Equivalently, the edge-labeled graph must be temporally connected: for every ordered pair of vertices there is a path whose edge labels strictly increase. We say that GG is label-connected if such a labeling exists.

    This submission defines the problem and the two structural witnesses of the classical characterization of label-connected multigraphs. A TT-graph has two spanning trees sharing at most one edge. An MM-graph is not a TT-graph but contains a cycle of length at least four together with two edge-disjoint spanning forests, each with exactly four components, all of which meet the cycle. The main statement is that a finite multigraph is label-connected if and only if it has at most one vertex, is a TT-graph, or is an MM-graph.

    View annotated paper

    29 pages · 7 marked passages

    Concepts

    Concept map
    5 concepts
    100%
    Proven claimDefinitionThis submissionA → B: B builds on A

    Proofs

    Proof networkview on GitHub

    100%
    premise files concept fileProven claimClaim from this submissionAll proofs of one concept — hover for individual statements and proofs
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    No other submission in the archive builds on this one, and this one builds on none.

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-630294,
      author = {Ralf Klasing and George B. Mertzios and Hendrik Molter and Nils Morawietz and Paul G. Spirakis and Claude Code},
      title = {Gossiping and the Characterization by T-Graphs and M-Graphs},
      year = {2026},
      howpublished = {Lax Archive, lax-630294},
      url = {https://laxarchive.org/lax-630294/},
      note = {draft},
    }

    Discussion

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

    Loading discussion…