Lax Lean Archive

Path Replacement of a Regular Multigraph

Lax920634.PathReplacement · concepts/Lax920634/PathReplacement.lean · lax-920634

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

    Replace every vertex of a degree-dd multigraph by a path of dd ports, then join ports paired by the edge-reversing involution. Every port has at most two path neighbors and one neighbor across an original edge. The resulting simple graph is subcubic.

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

    Lean source view on GitHub

    1import Lax920634.EdgeExpansion
    2
    3/-!
    4---
    5title: Path Replacement of a Regular Multigraph
    6type: definition
    7---
    8Replace every vertex of a degree-dd multigraph by a path of dd ports,
    9then join ports paired by the edge-reversing involution. Every port has at
    10most two path neighbors and one neighbor across an original edge. The
    11resulting simple graph is subcubic.
    12
    13# Formalization notes
    14
    15The port map need not pair distinct ports; loops and repeated edges in the
    16base graph are allowed. The undirected closure removes any loops and
    17identifies coincident edges. Base cut cardinalities count darts, preserving
    18the base multiplicities. Each crossing base edge has one source-side dart.
    19-/
    20
    21namespace Lax920634.PathReplacement
    22
    23/-- Replace each base vertex by a path of its ports and add the paired-port edges. -/
    24def graph {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d) :
    25 SimpleGraph (Fin n × Fin d) :=
    26 SimpleGraph.fromRel (fun u v =>
    27 (u.1 = v.1 ∧ u.2.val + 1 = v.2.val) ∨ v = R u)
    28
    29/-- Base boundary darts with source in `S` and target outside `S`. -/
    30def baseCut {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d)
    31 (S : Set (Fin n)) : Set (Fin n × Fin d) :=
    32 {p | p.1 ∈ S ∧ (R p).1 ∉ S}
    33
    34end Lax920634.PathReplacement
    35
    Formalization notes

    The port map need not pair distinct ports; loops and repeated edges in the base graph are allowed. The undirected closure removes any loops and identifies coincident edges. Base cut cardinalities count darts, preserving the base multiplicities. Each crossing base edge has one source-side dart.

    Builds on
    Used by
    From Mathlib

    none

    Discussion

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

    Loading discussion…