FormalConjectures/WrittenOnTheWallII/GraphConjecture33.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 33

Reference: E. DeLaVina, Written on the Wall II, Conjectures of Graffiti.pc

Imports (1)
Imported by 1 file
  1. theorem WrittenOnTheWallII.GraphConjecture33.conjecture33 WOWII Conjecture 33 For a simple connected graph sorry line 49 source

    Source documentation

    WOWII Conjecture 33

    For a simple connected graph $G$, $\operatorname{path}(G) \ge \lceil 2 \operatorname{dist}\_{\operatorname{avg}}(M, V) \rceil$, where $\operatorname{path}(G)$ is the number of vertices of a largest induced path of $G$, $M$ is the set of maximum-degree vertices, and $\operatorname{dist}\_{\operatorname{avg}}(M, V)$ is the average of all nonzero distances $\operatorname{dist}\_G(m, v)$ with $m \in M$ and $v \in V$.

    The conjecture is false: the source records an October 2005 counterexample with $\operatorname{path}(G) = 7$ and $\operatorname{dist}\_{\operatorname{avg}}(M, V) = 3.56$.

    L4DEL explanation

    WOWII Conjecture 33 For a simple connected graph $G$, $\operatorname{path}(G) \ge \lceil 2 \operatorname{dist}\_{\operatorname{avg}}(M, V) \rceil$, where $\operatorname{path}(G)$ is the number of vertices of a largest induced path of $G$, $M$ is the set of maximum-degree vertices, and $\operatorname{dist}\_{\operatorname{avg}}(M, V)$ is the average of all nonzero distances $\operatorname{dist}\_G(m, v)$ with $m \in M$ and $v \in V$. The conjecture is false: the source records an October 2005 counterexample with $\operatorname{path}(G) = 7$ and $\operatorname{dist}\_{\operatorname{avg}}(M, V) = 3.56$.

    Sources and attribution: Pinned Lean source (1646ca16afd6)

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, Set, Set.ofPred, Eq, Nat, SimpleGraph.degree, Membership.mem, SimpleGraph.neighborSet, SimpleGraph.maxDegree, Real, Finset, Prod and 17 more

    Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

    48 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

    theorem conjecture33 : answer(False) ↔
    ∀ (α : Type) [Fintype α] [DecidableEq α] [Nontrivial α]
      (G : SimpleGraph α) [DecidableRel G.Adj] (h : G.Connected),
      let M : Set α := {v | G.degree v = G.maxDegree}
…
  2. example WrittenOnTheWallII.GraphConjecture33.(example at line 64) line 64 source

    Source documentation

    The path G invariant cast to ℤ is nonneg.

    example (G : SimpleGraph (Fin 3)) : 0 ≤ (path G : ℤ) := Int.natCast_nonneg _
…
  3. example WrittenOnTheWallII.GraphConjecture33.(example at line 68) line 68 source

    Source documentation

    In K₃, the max degree is 2.

    example : (⊤ : SimpleGraph (Fin 3)).maxDegree = 2 := by decide
…