brualdi-ch13-10

open

difficulty 4

credited

Run this goal:./swarm/run.sh --goal brualdi-ch13-10

What it runs

The Lean statement the swarm must prove — kernel-verified at Gate A. The trailing sorry is the open obligation a proof replaces.

goals/brualdi-ch13-10.lean

import Mathlib

universe u
structure IsTournament {V : Type u} (G : Digraph V) : Prop where
  irrefl : ∀ (u : V), ¬ G.Adj u u
  adj : ∀ (u v : V), u ≠ v → (G.Adj u v ↔ ¬ G.Adj v u)
inductive Digraph.Walk {V : Type u} (G : Digraph V) : V → V → Type u
  | nil {u : V} (h : G.Adj u u) : Digraph.Walk G u u
  | cons {u v w : V} (h : G.Adj u v) (p : Digraph.Walk G v w) : Digraph.Walk G u w
  deriving DecidableEq
def Digraph.Walk.support {V : Type u} {G : Digraph V} {u v : V} : Digraph.Walk G u v → List V
  | .nil h => [u]
  | .cons _ p => u :: p.support
def Digraph.Walk.IsPath {V : Type u} {G : Digraph V} {u v : V} (p : Digraph.Walk G u v) : Prop :=
  p.support.Nodup
def Digraph.Walk.length {V : Type u} {G : Digraph V} {u v : V} : Digraph.Walk G u v → ℕ
  | .nil h => 0
  | .cons _ p => 1 + p.length

theorem brualdi_ch13_10 {V : Type u} (T : Digraph V) (hT : IsTournament T) :
    ∃ (u : V), ∀ (x : V), ∃ (p : T.Walk u x), p.IsPath ∧ p.length ≤ 2 := by
  sorry

Runs (0)

No runs recorded for this suite yet — they appear here as the swarm attempts the benchmarks.