IndisputableMonolith.Causality.ConeBound

   1import Mathlib
   2
   3namespace IndisputableMonolith
   4namespace Causality
   5
   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 =>
  40    intro y
  41    simp [ballFS, ballP, Finset.mem_singleton]
  42  | succ n ih =>
  43    intro y
  44    dsimp [ballFS, ballP]
  45    constructor
  46    · intro hy
  47      have : y ∈ ballFS (α:=α) x n ∨ y ∈ (ballFS (α:=α) x n).biUnion (fun z => B.neighbors z) :=
  48        Finset.mem_union.mp hy
  49      cases this with
  50      | inl hy_prev => exact Or.inl ((ih _).mp hy_prev)
  51      | inr hy_union =>
  52        rcases Finset.mem_biUnion.mp hy_union with ⟨z, hz, hyz⟩
  53        refine Or.inr ⟨z, (ih z).mp hz, ?_⟩
  54        dsimp [KB]
  55        rw [B.step_iff_mem]
  56        exact hyz
  57    · intro hy
  58      cases hy with
  59      | inl hy0 =>
  60        have : y ∈ ballFS (α:=α) x n := (ih y).mpr hy0
  61        exact Finset.mem_union.mpr (Or.inl this)
  62      | inr hy1 =>
  63        rcases hy1 with ⟨z, hz, hstep⟩
  64        have hz' : z ∈ ballFS (α:=α) x n := (ih z).mpr hz
  65        have hstep' : y ∈ B.neighbors z := by
  66          rw [← B.step_iff_mem]
  67          exact hstep
  68        have hy_union : y ∈ (ballFS (α:=α) x n).biUnion (fun z => B.neighbors z) :=
  69          Finset.mem_biUnion.mpr ⟨z, hz', hstep'⟩
  70        exact Finset.mem_union.mpr (Or.inr hy_union)
  71theorem card_singleton {x : α} : ({x} : Finset α).card = 1 :=
  72  Finset.card_singleton x
  73theorem card_union_le (s t : Finset α) : (s ∪ t).card ≤ s.card + t.card :=
  74  Finset.card_union_le s t
  75theorem card_bind_le_sum (s : Finset α) (f : α → Finset α) :
  76  (s.biUnion f).card ≤ Finset.sum s (fun z => (f z).card) :=
  77  Finset.card_biUnion_le
  78theorem sum_card_neighbors_le (s : Finset α) :
  79  Finset.sum s (fun z => (B.neighbors z).card) ≤ d * s.card := by
  80  have h1 : Finset.sum s (fun z => (B.neighbors z).card) ≤ Finset.sum s (fun _ => d) := by
  81    apply Finset.sum_le_sum
  82    intro z _
  83    exact B.degree_bound_holds z
  84  have h2 : Finset.sum s (fun _ => d) = s.card * d := by
  85    simp [Finset.sum_const]
  86  rw [h2, Nat.mul_comm] at h1
  87  exact h1
  88theorem card_bind_neighbors_le (s : Finset α) :
  89  (s.biUnion (fun z => B.neighbors z)).card ≤ d * s.card := by
  90  have h1 := card_bind_le_sum s (fun z => B.neighbors z)
  91  have h2 := sum_card_neighbors_le s
  92  exact Nat.le_trans h1 h2
  93theorem card_ballFS_succ_le (x : α) (n : Nat) :
  94  (ballFS (α:=α) x (n+1)).card ≤ (1 + d) * (ballFS (α:=α) x n).card := by
  95  dsimp [ballFS]
  96  let prev := ballFS (α:=α) x n
  97  let new_neighbors := prev.biUnion (fun z => B.neighbors z)
  98  have h_union := card_union_le prev new_neighbors
  99  have h_neighbors := card_bind_neighbors_le prev
 100  have h_combined : (prev ∪ new_neighbors).card ≤ prev.card + d * prev.card :=
 101    Nat.le_trans h_union (Nat.add_le_add_left h_neighbors prev.card)
 102  calc (prev ∪ new_neighbors).card
 103    ≤ prev.card + d * prev.card := h_combined
 104    _ = (1 + d) * prev.card := by ring
 105theorem ballFS_card_le_geom (x : α) : ∀ n : Nat, (ballFS (α:=α) x n).card ≤ (1 + d) ^ n := by
 106  intro n
 107  induction n with
 108  | zero =>
 109    dsimp [ballFS, Nat.pow_zero]
 110    rw [card_singleton]
 111  | succ n ih =>
 112    have h_succ := card_ballFS_succ_le x n
 113    calc (ballFS x (n + 1)).card
 114      ≤ (1 + d) * (ballFS x n).card := h_succ
 115      _ ≤ (1 + d) * ((1 + d) ^ n) := Nat.mul_le_mul_left (1 + d) ih
 116      _ = (1 + d) ^ (n + 1) := by
 117        rw [Nat.pow_succ]
 118        ring
 119
 120end ConeBound
 121end Causality
 122end IndisputableMonolith
 123