Lax Lean Archive

Path Replacement Preserves Uniform Expansion

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

proven

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

    Lemma

    Suppose a degree-dd regular port involution has at least a quarter of the degree times the smaller cut side in boundary darts, and d≥2d\ge2. Replacing its vertex clouds by paths gives edge expansion at least 1/(8d)1/(8d).

    Full clouds of a cut form a small base set. Each partial cloud contributes a distinct crossing path edge. The base edges leaving full clouds either cross the final cut or reach partial clouds. Counting these two possibilities bounds the size of the cut by 8d8d times its edge boundary.

    Concept map
    3 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Lax920634.PathReplacement
    2
    3/-!
    4---
    5title: Path Replacement Preserves Uniform Expansion
    6type: lemma
    7---
    8Suppose a degree-dd regular port involution has at least a quarter of the
    9degree times the smaller cut side in boundary darts, and d≥2d\ge2.
    10Replacing its vertex clouds by paths gives edge expansion at least 1/(8d)1/(8d).
    11
    12Full clouds of a cut form a small base set. Each partial cloud contributes
    13a distinct crossing path edge. The base edges leaving full clouds either
    14cross the final cut or reach partial clouds. Counting these two possibilities
    15bounds the size of the cut by 8d8d times its edge boundary.
    16
    17# Formalization notes
    18
    19The base cut counts darts to preserve multigraph multiplicity. The target is
    20a simple graph; the argument tolerates loops and overlaps between matching
    21edges and path edges.
    22-/
    23
    24namespace Lax920634.PathExpansion
    25
    26open PathReplacement EdgeExpansion Function
    27
    28/-- An expanding regular port involution yields a uniformly expanding path replacement. -/
    29axiom replacement_expansion {n d : ℕ} (R : Fin n × Fin d → Fin n × Fin d)
    30 (hR : Involutive R) (hd : 2 ≤ d)
    31 (hbase : ∀ U : Set (Fin n),
    32 d * min U.ncard (n - U.ncard) ≤ 4 * (baseCut R U).ncard) :
    33 HasEdgeExpansionAtLeast (graph R) (1 / (8 * (d : ℚ)))
    34
    35end Lax920634.PathExpansion
    36
    Show Proof
    Formalization notes

    The base cut counts darts to preserve multigraph multiplicity. The target is a simple graph; the argument tolerates loops and overlaps between matching edges and path edges.

    Builds on
    Used by

    none

    From Mathlib

    none

    Discussion

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

    Loading discussion…