The general step (`chunkL_from`)

The general step: blocks from a cut st of chunk c.

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

theorem J6Seg.chunkL_from (hl : 1 ≤ lam) (c : ℕ) :
    ∀ (f st : ℕ) (x : List ℤ), c * lam ≤ st → st ≤ c * lam + lam → cutP s t lam st ∨ s ≤ st →
      c * lam + lam ≤ st + f → x.length = c * lam + lam - st →
      ∀ (X : ℕ → ℤ), (∀ u < x.length, x.getD u 0 = X (st + u)) →
      ∀ u < x.length, (chunkL P (diL P R s t lam α) (giL P R s t lam α) (gamL P R s t lam α)
        (ddL P R s t lam α) (descsFrom P R s t lam α c f st) x).getD u 0 =
        if st + u < s then applyMinv P (TT P R s t α) (BB s t lam w) X (st + u) else 0

Context. Segmented inverse (S2), machine side 2: M⁻¹ chunk by chunk

With λ-aligned chunks [cλ, cλ + λ) every block of mkBlocks s t λ w lies inside one chunk (cuts at the multiples of λ). The blocks of chunk c (chunkBl) start at cλ and follow each other (b ↦ b + 1 + enF b) until min(s, cλ + λ).

• chunkL di gi gam dd descs x: the block solves of consecutive blocks descs = [(n_k, am_k, ap_k)] on consecutive segments of x, zeros on the rest;
• descsOf T c: the block descriptors of chunk c (lengths and the block tables am, ap);
• chunkL_rep: on chunk c, chunkL … (descsOf c) x is M⁻¹ (applyMinv) at the positions < s of the chunk and 0 at the others.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).