BoundedStep

formal source

   6/-! Minimal ConeBound: local definitions to avoid heavy imports. Provides
   7    ball growth bounds under a bounded-degree step relation. -/
   8
   9class BoundedStep (α : Type) (degree_bound : outParam Nat) where
  10  step : α → α → Prop
  11  neighbors : α → Finset α
  12  step_iff_mem : ∀ x y, step x y ↔ y ∈ neighbors x
  13  degree_bound_holds : ∀ x, (neighbors x).card ≤ degree_bound
  14
  15structure Kinematics (α : Type) where
  16  step : α → α → Prop
  17
  18def ballP {α : Type} (K : Kinematics α) (x : α) : Nat → α → Prop
  19| 0, y => y = x
  20| Nat.succ n, y => ballP K x n y ∨ ∃ z, ballP K x n z ∧ K.step z y
  21
  22namespace ConeBound
  23
  24variable {α : Type} {d : Nat}
  25variable [DecidableEq α]
  26variable [B : BoundedStep α d]
  27
  28def KB : Kinematics α := { step := B.step }
  29
  30noncomputable def ballFS (x : α) : Nat → Finset α
  31| 0 => {x}
  32| Nat.succ n =>
  33    let prev := ballFS x n
  34    prev ∪ prev.biUnion (fun z => B.neighbors z)
  35
  36theorem mem_ballFS_iff_ballP (x : α) : ∀ n y, y ∈ ballFS (α:=α) x n ↔ ballP (KB (α:=α)) x n y := by
  37  intro n
  38  induction n with
  39  | zero =>