proof

P24 Weakest handle capacity / CCI

Lean spine source

Declarations: P24_chain_capacity_le_each_edge

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P24_chain_capacity_le_each_edge :
    ∀ (xs : List Int) (e : Int), e ∈ xs → ChainCapacity xs ≤ e := by
  intro xs
  induction xs with
  | nil => intro e he; simp at he
  | cons a as ih =>
      intro e he
      cases as with
      | nil =>
          rcases List.mem_singleton.mp he with rfl
          rfl
      | cons b bs =>
          simp only [List.mem_cons] at he
          have hcc : ChainCapacity (a :: b :: bs) = min a (ChainCapacity (b :: bs)) := rfl
          rcases he with rfl | he'
          · rw [hcc]
            exact min_le_left _ _
          · exact le_trans (min_le_right _ _) (ih e (by simp only [List.mem_cons]; exact he'))