brk_all (KFY 6: generic combinators for the line passes)

The following holds (Lean statement, in the scope of module Solutions.KFY6Gen):

theorem NLogN.KFY.brk_all (M : MulSpec) (l : List (Fin HS × Ex HS)) (P : RM) (t : IState HS) (j : Fin HS)
    (Z : List Item) (C B K : ℕ) (hl : PushOk l t) (hj : j ∉ l.map Prod.fst)
    (hB : ∀ p ∈ l, p.2.Bnd t B ∧ p.2.size ≤ K ∧ zsz (p.2.eval t) ≤ B)
    (hP : P.run ((NLogN.KFY.pushL l).run t) = ((NLogN.KFY.pushL l).run t).upd j Z ∧ P.ok M ((NLogN.KFY.pushL l).run t) ∧
      P.cost M ((NLogN.KFY.pushL l).run t) ≤ C) :
    (brk l P).run t = t.upd j Z ∧ (brk l P).ok M t ∧
      (brk l P).cost M t ≤ brkC l.length K B C

Context. The lemma belongs to the part KFY 6: generic combinators for the line passes.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.