`Kinematics`

definition

show as: view math explainer →

module: IndisputableMonolith.Causality.ConeBound
domain: Causality
line: 15 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Causality.ConeBound on GitHub at line 15.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  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 =>
  40    intro y
  41    simp [ballFS, ballP, Finset.mem_singleton]
  42  | succ n ih =>
  43    intro y
  44    dsimp [ballFS, ballP]
  45    constructor

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.