The `B₀` pass of the machine in the round-six regime (round six, `r6_passB`)

The B₀ pass of the machine in the round-six regime.

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

theorem J6Seg.r6_passB (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
    SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
    ∀ [∀ i, NeZero (sD6 src D i)] [∀ i, NeZero (tD6 P n D i)],
    ∀ M : AxisMaps6 (αN6 P n) (sD6 src D) (tD6 P n D), FitSpec6 P n src D M →
    ∀ (ys : List GI) (y : ((i : Fin (D + 1)) → ZMod (tD6 P n D i)) → ℂ),
      RepFull (pP6 P n) (tD6 P n D) ys y → ‖y‖ ≤ 1 →
      RepPad (pP6 P n) (sD6 src D) (tD6 P n D)
          (tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys)
          (vOf (pP6 P n) (sD6 src D) (tD6 P n D)
            (tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys)) ∧
        NLogN.KFB.GB (pP6 P n + 2) (tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys) ∧
        ‖vOf (pP6 P n) (sD6 src D) (tD6 P n D)
            (tensorGo (mapsLine6 P n src D) (List.ofFn (tD6 P n D)) ys) -
          tensCLM (kerB M.B) y‖ ≤ errW6 P n * hp (pP6 P n)

Context. Segmented inverse (S2), machine side 12: the B₀ pass in the round-six regime

• LJ_length_ge: the near-boundary line has at least 2w + 1 positions ([0,w), [s-w,s) and the cut λ), so the cyclic coupling window K = w fits;
• FitSpec6 M: the per-axis properties of r6_axisMaps_fit (‖B_i‖ ≤ 1/2, the S̃ and B̃₀ bounds, B̃₀ 0 = 0); r6_fitSpec: such M exist for n ≥ n₁;
• mapsLine6: the machine's line maps (lineB with λ = lamP d, w = K = wF d, n_c = t_i/λ, R = ⌊p/7⌋, P = segPF p d s_i);
• r6_passB: for n ≥ n₁, every source list, every M with FitSpec6 M and every RepFull ys y, ‖y‖ ≤ 1: the tensorGo of the machine's line maps is RepPad of a v with GB (p+2) and ‖v − tensCLM (kerB M.B) y‖ ≤ errW6 · 2^{-p} — the representation and error part of the eB clause of LineBody6.

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*).