FormalConjectures/WrittenOnTheWallII/GraphConjecture109.lean

GitHub source file

3 declarations, 1 contain sorry, 0 declared as axioms

Written on the Wall II - Conjecture 109

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

Imports (1)
  1. theorem WrittenOnTheWallII.GraphConjecture109.conjecture109 sorry line 55 source

    depends on sorry what this means

    Statement uses: Iff, False, Fintype, DecidableEq, Nontrivial, SimpleGraph, DecidableRel, SimpleGraph.Adj, SimpleGraph.Connected, LE.le, Real, SimpleGraph.indepNum, Int.floor, HDiv.hDiv, HAdd.hAdd, SimpleGraph.residue, HMul.hMul, OfNat.ofNat, Nat, SimpleGraph.b

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

    38 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  2. example WrittenOnTheWallII.GraphConjecture109.(example at line 65) line 65 source

    Source documentation

    The invariant b G is nonneg (cast of a natural number).

    example (G : SimpleGraph (Fin 3)) : 0 ≤ b G := Nat.cast_nonneg _
…
  3. example WrittenOnTheWallII.GraphConjecture109.(example at line 70) line 70 source

    Source documentation

    The residue of $K_2$ equals $1$: degree sequence is $[1, 1]$; one Havel-Hakimi step gives $[0]$, leaving a single zero.

    example : residue (⊤ : SimpleGraph (Fin 2)) = 1 := by
…