Lax Lean Archive

Arbitrarily Large Subcubic Expanders

Lax920634.ExpanderExistence · concepts/Lax920634/ExpanderExistence.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

    Theorem

    For every size threshold there is a finite simple subcubic graph above that threshold with edge expansion at least 1/(8d)1/(8d), where d=D2d=D^2 is fixed. The witnesses are generated by the specified deterministic polynomial-time construction.

    Concept map
    5 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.ZigZagConstruction
    2
    3/-!
    4---
    5title: Arbitrarily Large Subcubic Expanders
    6type: theorem
    7---
    8For every size threshold there is a finite simple subcubic graph above that
    9threshold with edge expansion at least 1/(8d)1/(8d), where d=D2d=D^2 is fixed.
    10The witnesses are generated by the specified deterministic polynomial-time
    11construction.
    12
    13# Formalization notes
    14
    15Graphs use canonical carriers `Fin n`. The threshold may be exceeded;
    16the level-selection algorithm keeps the excess within a fixed constant factor.
    17-/
    18
    19namespace Lax920634.ExpanderExistence
    20
    21open ZigZagConstruction EdgeExpansion
    22
    23/-- There are arbitrarily large finite simple subcubic expanders with one fixed constant. -/
    24axiom exists_subcubic_expander (lower : ℕ) :
    25 ∃ n : ℕ, ∃ G : SimpleGraph (Fin n), lower ≤ n ∧
    26 IsSubcubic G ∧
    27 HasEdgeExpansionAtLeast G (1 / (8 * (degree : ℚ)))
    28
    29end Lax920634.ExpanderExistence
    30
    Show Proof
    Formalization notes

    Graphs use canonical carriers FinnFin n. The threshold may be exceeded; the level-selection algorithm keeps the excess within a fixed constant factor.

    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…