FormalConjectures/WrittenOnTheWallII/GraphConjecture430a.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

4 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 430a

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

The conjecture is false for the nonuniform clique blow-up of P₇ with blob orders (1,4,12,19,12,4,1). Its independent domination number is three, its center-neighborhood independence number is two, and its Caro--Wei sum is less than two. The claimed inequality therefore becomes 3 ≤ 2.

Imports (1)
  1. def WrittenOnTheWallII.GraphConjecture430a.centerFinset The center of a finite graph line 40 source

    Source documentation

    The center of a finite graph.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, Finset

    Proof uses: Finset.filter, Eq, ENat, SimpleGraph.eccent, SimpleGraph.radius, Finset.univ

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    noncomputable def centerFinset {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) : Finset V := by
…
  2. def WrittenOnTheWallII.GraphConjecture430a.setNeighborhood DeLaViña's N(S): the union of open vertex neighborhoods line 47 source

    Source documentation

    DeLaViña's N(S): the union of open vertex neighborhoods. This may intersect S.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Finset

    Proof uses: Finset.filter, Exists, And, Membership.mem, Finset.univ

    3 instances, coercions and auxiliary constants left out.

    def setNeighborhood {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] (S : Finset V) : Finset V :=
…
  3. def WrittenOnTheWallII.GraphConjecture430a.caroWei The exact rational Caro--Wei sum line 52 source

    Source documentation

    The exact rational Caro--Wei sum.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Fintype, DecidableEq, SimpleGraph, DecidableRel, SimpleGraph.Adj, Rat

    Proof uses: Finset.sum, Finset.univ, HDiv.hDiv, OfNat.ofNat, HAdd.hAdd, Nat, SimpleGraph.degree, Membership.mem, Set, SimpleGraph.neighborSet

    12 instances, coercions and auxiliary constants left out.

    def caroWei {V : Type*} [Fintype V] [DecidableEq V]
    (G : SimpleGraph V) [DecidableRel G.Adj] : ℚ :=
…
  4. theorem WrittenOnTheWallII.GraphConjecture430a.conjecture430a sorry line 64 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nonempty, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LT.lt, Nat, OfNat.ofNat, Fintype.card, LE.le, Int, SimpleGraph.indepDominationNumber, HAdd.hAdd, SimpleGraph.indepNum, Finset, WrittenOnTheWallII.GraphConjecture430a.setNeighborhood and 7 more

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

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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