The native `J` set-up (round six, `eJn_sp`)

The native J set-up.

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

theorem J6Seg.PJ.eJn_sp (kA kC wA wC : ℕ) {k pre post s t p α d W N B : ℕ} {Zn : Fin HS}
    (hZ : Zn ∉ rg) (hZ5 : Zn.val < 56) (hZT : Zn ≠ sTmp) (hZC : Zn ≠ cRdC)
    (hZv : Zn.val = 49 ∨ Zn.val = 55)
    (oN : Fin 19 → Fin HS) (hinj : Injective oN) (hlt : ∀ i, (oN i).val < 56)
    (hx : ∀ i, oN i ≠ sX ∧ oN i ≠ sLn ∧ oN i ≠ sOut ∧ oN i ≠ sT2 ∧ oN i ≠ cLC) (hZo : ∀ i, oN i ≠ Zn)
    (hW : parBig kA kC wA wC k pre post s t p α d < 2 ^ W)
    (hNW : N < 2 ^ W) (hW4 : 4 ≤ W) (hN5 : 5 ≤ N)
    (hs : 0 < s) (hws : wF d ≤ s) (hQW : segPF p d s ≤ W)
    (hsN : s ≤ N) (hlN : lamP d ≤ N) (hNMN : lamP d * (2 * wF d + 1) ≤ N)
    (hmm : (LJ s t (lamP d) (wF d)).length * (LJ s t (lamP d) (wF d)).length ≤ N)
    (hmc : (LJ s t (lamP d) (wF d)).length * (2 * wF d + 2) ≤ N)
    (bss : s * s ≤ 2 ^ W) (hlw : lamP d + wF d ≤ 2 ^ W)
    (hW8 : 8 * ((LJ s t (lamP d) (wF d)).length + 1) ^ 2 ≤ 2 ^ W)
    (hJB : JB (segPF p d s) (p / 7) W s t α (lamP d) (wF d))
    (hMb : ∀ q ≤ (LJ s t (lamP d) (wF d)).length, ∀ i < (LJ s t (lamP d) (wF d)).length,
      ∀ k < (LJ s t (lamP d) (wF d)).length,
      |Mseq (segPF p d s) (bandS (lamP d + wF d) (s - lamP d - wF d)) (LJ s t (lamP d) (wF d))
        (capI (segPF p d s) (mkTables (segPF p d s) (p / 7) s t α) (mkBlocks s t (lamP d) (wF d)))
        q i k| ≤ 2 ^ W)
    (hbl : (JK.jBody (kA * segPF p d s + kC) (JK.jFs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jBs (segPF p d s) (p / 7) s t (lamP d) (wF d) α)
      (JK.jCc (segPF p d s) (p / 7) s t (lamP d) (wF d) α (wF d))).length ≤ 2 ^ W)
    (hvB : ∀ a ∈ cVals (wA * segPF p d s + wC) (Nat.clog 2 (LJ s t (lamP d) (wF d)).length) pre 1
      post, zsz a ≤ B)
    (hlB : zsz ((tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
      (kA * segPF p d s + kC)) 1).length : ℤ) ≤ B)
    (hTB : Bnd B (tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
      (kA * segPF p d s + kC)) 1))
    (s0 : IState HS) :
    Sp (eJn kA kC wA wC Zn oN) (encK s0 (F0 Zn (dsc k pre post s t p α d)))
      (encK s0 (extend oN (kerRegs (wA * segPF p d s + wC) (wA * segPF p d s + wC)
        (Nat.clog 2 (LJ s t (lamP d) (wF d)).length) pre 1 post
        (tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
          (kA * segPF p d s + kC)) 1))
        (F0 Zn (dsc k pre post s t p α d))))
      (cEJn kA kC wA wC W N d s p (LJ s t (lamP d) (wF d)).length B
        (tabsT (fun _ => jTabX (segPF p d s) (p / 7) s t (lamP d) (wF d) α
          (kA * segPF p d s + kC)) 1).length)

Context. B5 J side, part K28: the native J set-up eJn

eJn = initP rg; eJcore; finiP rg; distAll oN: from the descriptor alone on Zn ∈ {49, 55} to the J-pass register file kerRegs wd wd ⌈log₂ m⌉ pre 1 post (tabsT (fun _ => jTab) 1) on oN (eJn_sp). The tear-down is the chunk side's tearP.

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