P24 Weakest handle capacity / CCI

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'))

/-- Measurement convention: every system has a *designated* measured correction
    path (which agent the deployment treats as corrector, which handles it
    audits, which capacities it measured). This is data-level vocabulary in the
    same class as `CCIPenaltiesSys` — it asserts **no** validity property. In
    particular it does *not* assert control, persistence, or absence of
    capture; those live in `CorrectionPathLegitimate` and are only available
    through the labeled bridge `MB4a` below (or as explicit hypotheses). -/