The native `J` pair on every axis (round six, `j_native`)
ProvedJ6Seg.PJ.j_nativeThe native J pair on every axis.
The following holds (Lean statement, in the scope of module Solutions.J6SegILPreJK33):
theorem J6Seg.PJ.j_native (P : Prm) (hP : P.Ok) (pl : Plan6) {Zn : Fin HS} {oN : Fin 19 → Fin HS}
(hZ : Zn ∉ rg) (hZ5 : Zn.val < 56) (hZT : Zn ≠ sTmp) (hZC : Zn ≠ cRdC)
(hZv : Zn.val = 49 ∨ Zn.val = 55) (hZL : Zn ≠ cLC)
(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) :
∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
∀ k ≤ D, ∀ A' : ℕ, ∃ cU cD : ℕ,
(∀ s0, Sp (eJn pl.kA pl.kC pl.wA pl.wC Zn oN) (encK s0 (F0 Zn (descAx6 P n src D k)))
(encK s0 (extend oN (jRegs6 P n src D k pl) (F0 Zn (descAx6 P n src D k)))) cU) ∧
(∀ s0, Sp (tearP oN) (encK s0 (extend oN (jRegs6 P n src D k pl)
(F0 Zn (descAx6 P n src D k)))) (encK s0 (F0 Zn (descAx6 P n src D k))) cD) ∧
((cU + 2 : ℕ) : ℝ) ≤ cU6 P n A' / (D + 1) ∧
((cD + 2 : ℕ) : ℝ) ≤ cU6 P n A' / (D + 1)
Context. B5 J side, part K33: the native J pair on every axis, within budget
j_native: eventually, on every axis, eJn builds jRegs6 from the descriptor and tearP
clears it, each at cost + 2 ≤ cU6 P n A' / (D + 1).
The widths: W = (20 + 2kA + wA)·Q + 2kC + wC + 1600, N = (s+1)²(2w+2) + λ(2w+1) + 5,
B = W + kJ + 8; every quantity of the line is < 2^Q =: E and all bounds are ≤ 2^20 E^19.
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*).
-- Round-six κ development (integer-multiplication-kappa), generated by skeleton subtraction. import Definitions.Def_IntMul_Kappa_R6_Defs71 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open J6Seg J6Seg.PJ set_option maxRecDepth 100000 open IntMul NLogN NLogN.KIL NLogN.RS Function IntMul.Kappa.R6 J6Seg.Side
theorem J6Seg.PJ.j_native (P : Prm) (hP : P.Ok) (pl : Plan6) {Zn : Fin HS} {oN : Fin 19 → Fin HS}
(hZ : Zn ∉ rg) (hZ5 : Zn.val < 56) (hZT : Zn ≠ sTmp) (hZC : Zn ≠ cRdC)
(hZv : Zn.val = 49 ∨ Zn.val = 55) (hZL : Zn ≠ cLC)
(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) :
∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ, SrcOK6 P n src → ∀ D : ℕ, dP6 P n = D + 1 →
∀ k ≤ D, ∀ A' : ℕ, ∃ cU cD : ℕ,
(∀ s0, Sp (eJn pl.kA pl.kC pl.wA pl.wC Zn oN) (encK s0 (F0 Zn (descAx6 P n src D k)))
(encK s0 (extend oN (jRegs6 P n src D k pl) (F0 Zn (descAx6 P n src D k)))) cU) ∧
(∀ s0, Sp (tearP oN) (encK s0 (extend oN (jRegs6 P n src D k pl)
(F0 Zn (descAx6 P n src D k)))) (encK s0 (F0 Zn (descAx6 P n src D k))) cD) ∧
((cU + 2 : ℕ) : ℝ) ≤ cU6 P n A' / (D + 1) ∧
((cD + 2 : ℕ) : ℝ) ≤ cU6 P n A' / (D + 1) := by sorry