In the round-six regime the machine's line maps are the `B0seg` maps, and `λ ∣ t_i`, `s_i ≤ t_i` (`r6_maps_eq`)

In the round-six regime the machine's line maps are the B0seg maps, and λ ∣ t_i, s_i ≤ t_i.

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

theorem J6Seg.r6_maps_eq (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)],
    mapsLine6 P n src D = mapsBs (pP6 P n) (pP6 P n / 7) (lamP (dP6 P n)) (J6Seg.wF (dP6 P n))
      (αN6 P n) (segPF (pP6 P n) (dP6 P n)) (sD6 src D) (tD6 P n D) ∧
    ∀ i : Fin (D + 1), lamP (dP6 P n) ∣ tD6 P n D i ∧ sD6 src D i ≤ tD6 P n D i

Context. B-line machine, sweep 4: the machine computes tensorGo mapsLine6

• pipeSweep: the machine applies an axis program Fp k for k = 0, 1, … in place;
• pipeSweep_eq: if every Fp k is the in-place axis map of F k, the machine is sweepL;
• sweepL_tensorGo': sweepL of line maps of slice form is tensorGo;
• r6_maps_eq: in the round-six regime mapsLine6 = mapsBs and λ ∣ t_i, s_i < t_i;
• r6_machine: in the round-six regime, the seven-pass machine (pipe6, axes 0..d-1) computes tensorGo (mapsLine6 P n src D) on every array of the right length.

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