Lax Lean Archive

Admissibility is bounded by topological shallow-minor density

Lax199508.AdmissibilityBound · concepts/Lax199508/AdmissibilityBound.lean · lax-199508

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

    If every depth-r topological minor of a graph G has at most d · |V| edges, then the (r+1)-admissibility of G is at most 1 + 6 · (r+1) · d³. This is the workhorse behind every bound of a generalized coloring number by an edge-density bound: sparse shallow topological minors force an ordering in which no vertex reaches many predecessors along disjoint short paths.

    The source lecture notes state this as Lemma 3.2 of Chapter 2 (2019/20 edition): for every r and every graph G, adm⁡r(G)≤1+6r⌈∇~r−1(G)⌉3\operatorname{adm}_r(G) \le 1 + 6r\lceil\tilde\nabla_{r-1}(G)\rceil^3, where ∇~\tilde\nabla is the topological grad.

    Concept map
    4 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 Lax199508.Admissibility
    2import Lax199508.ShallowTopologicalMinors
    3
    4/-!
    5---
    6title: Admissibility is bounded by topological shallow-minor density
    7type: theorem
    8---
    9If every depth-*r* topological minor of a graph *G* has at most
    10*d* · |V| edges, then the (*r*+1)-admissibility of *G* is at most
    111 + 6 · (*r*+1) · *d*³. This is the workhorse behind every bound of a
    12generalized coloring number by an edge-density bound: sparse shallow
    13topological minors force an ordering in which no vertex reaches many
    14predecessors along disjoint short paths.
    15
    16The source lecture notes state this as Lemma 3.2 of Chapter 2 (2019/20
    17edition): for every *r* and every graph *G*,
    18adm⁡r(G)≤1+6r⌈∇~r−1(G)⌉3\operatorname{adm}_r(G) \le 1 + 6r\lceil\tilde\nabla_{r-1}(G)\rceil^3, where
    19∇~\tilde\nabla is the topological grad.
    20
    21# Formalization notes
    22
    23Hypothesis and conclusion are the predicates of the two imported
    24definition concepts. The statement is the notes' Lemma 3.2 with its
    25radius index shifted by one: the notes pair a conclusion at radius *r*
    26with a hypothesis at depth *r*−1, and writing the conclusion at *r*+1
    27against a hypothesis at depth *r* keeps truncated natural subtraction
    28out of a concept statement. This is presentation only — the shifted form
    29ranges over exactly the instances *r* ≥ 1 of the notes' form, which are
    30all of its instances with a defined hypothesis, and the constant is the
    31notes' constant with *r* read as *r*+1.
    32
    33The natural number *d* plays the notes' ⌈∇~r−1(G)⌉\lceil\tilde\nabla_{r-1}(G)\rceil: the
    34hypothesis `HasTopologicalDensityAtMost G r d` says exactly that the
    35topological grad of *G* at depth *r* is at most *d*, and the notes
    36instantiate their lemma at the ceiling of that grad, the least natural
    37number with this property. The leading 1 of the bound is the vertex *v*
    38itself, which admissibility counts.
    39-/
    40
    41namespace Lax199508.AdmissibilityBound
    42
    43open Lax199508.Admissibility Lax199508.ShallowTopologicalMinors
    44
    45/-- A depth-`r` topological edge-density bound `d` for `G` bounds the
    46`(r+1)`-admissibility of `G` by `1 + 6 · (r+1) · d ^ 3`. -/
    47axiom adm_le_of_hasTopologicalDensityAtMost {n : ℕ} (G : SimpleGraph (Fin n))
    48 (r d : ℕ) (h : HasTopologicalDensityAtMost G r d) :
    49 adm G (r + 1) ≤ 1 + 6 * (r + 1) * d ^ 3
    50
    51end Lax199508.AdmissibilityBound
    52
    Show Proof
    Formalization notes

    Hypothesis and conclusion are the predicates of the two imported definition concepts. The statement is the notes' Lemma 3.2 with its radius index shifted by one: the notes pair a conclusion at radius r with a hypothesis at depth r−1, and writing the conclusion at r+1 against a hypothesis at depth r keeps truncated natural subtraction out of a concept statement. This is presentation only — the shifted form ranges over exactly the instances r ≥ 1 of the notes' form, which are all of its instances with a defined hypothesis, and the constant is the notes' constant with r read as r+1.

    The natural number d plays the notes' ⌈∇~r−1(G)⌉\lceil\tilde\nabla_{r-1}(G)\rceil: the hypothesis HasTopologicalDensityAtMostGrdHasTopologicalDensityAtMost G r d says exactly that the topological grad of G at depth r is at most d, and the notes instantiate their lemma at the ceiling of that grad, the least natural number with this property. The leading 1 of the bound is the vertex v itself, which admissibility counts.

    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…