The round-six parameters in `ℕ` form (`r6_axis_nat`)
ProvedJ6Seg.r6_axis_natThe round-six parameters in ℕ form: 0 < s < t, 2 ≤ α, 3 s ≤ α² (t - s) (α²θ ≥ 3),
6 d ≤ s, 48 d² ≤ α² ≤ p, p < 48 d (α+1)², 3072 ≤ b'.
The following holds (Lean statement, in the scope of module Solutions.J6SegR6):
theorem J6Seg.r6_axis_nat (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ j < dP6 P n,
0 < src j ∧ src j < tF6 P n j ∧ 2 ≤ αN6 P n ∧
3 * src j ≤ αN6 P n ^ 2 * (tF6 P n j - src j) ∧ 6 * dP6 P n ≤ src j ∧
48 * dP6 P n ^ 2 ≤ αN6 P n ^ 2 ∧ αN6 P n ^ 2 ≤ pP6 P n ∧
pP6 P n < 48 * dP6 P n * (αN6 P n + 1) ^ 2 ∧ 3072 ≤ b'P6 P n ∧ 1 ≤ dP6 P n
Context. Segmented inverse (S2): the round-six regime
r6_axis_hyps: for every P with P.Ok there is n₁ such that for n ≥ n₁, every admissible
source list (SrcOK6) and every axis j < d, the hypotheses of the segmented-inverse theorems
hold with s = src j, t = tF6 j, α = αN6:
0 < s < t, 2 ≤ α and α²θ = xθ s t α ≥ 3.
Proof: SrcOK6 forces the window w_j = ⌊t/(8d²)⌋ ≥ 1, so t - s ≥ w_j ≥ t/(16d²); and
α² ≥ 48 d² as soon as b' = b^{1+x} ≥ 3072 d³, which holds for large b because
d ≤ b^ε and 3ε < 1 + x (Prm.Ok.three_eps).
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_K_Defs33 import Definitions.Def_IntMul_Kappa_R6_Defs1 import Mathlib import Definitions.Def_IntMul_HvdH_M_Defs8 import Definitions.Def_IntMul_MultitapeModel import Definitions.Def_IntMul_HvdH_Numeric import Definitions.Def_IntMul_HvdH_ExpApprox import Definitions.Def_IntMul_HvdH_RealExp import Definitions.Def_IntMul_HvdH_Twiddle import Definitions.Def_IntMul_HvdH_SApprox import Definitions.Def_IntMul_HvdH_DiagApprox import Definitions.Def_IntMul_HvdH_EApprox import Definitions.Def_IntMul_HvdH_JApprox import Definitions.Def_IntMul_HvdH_BApprox import Definitions.Def_IntMul_HvdH_FPApprox import Definitions.Def_IntMul_HvdH_MachineRef import Definitions.Def_IntMul_KappaFramework import Definitions.Def_IntMul_KappaJainData import Definitions.Def_IntMul_Kappa_R6_Defs14 set_option autoImplicit false set_option relaxedAutoImplicit false set_option maxHeartbeats 1000000 open Real open IntMul.HvdH IntMul.Kappa.R6
theorem J6Seg.r6_axis_nat (P : Prm) (hP : P.Ok) : ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
SrcOK6 P n src → ∀ j < dP6 P n,
0 < src j ∧ src j < tF6 P n j ∧ 2 ≤ αN6 P n ∧
3 * src j ≤ αN6 P n ^ 2 * (tF6 P n j - src j) ∧ 6 * dP6 P n ≤ src j ∧
48 * dP6 P n ^ 2 ≤ αN6 P n ^ 2 ∧ αN6 P n ^ 2 ≤ pP6 P n ∧
pP6 P n < 48 * dP6 P n * (αN6 P n + 1) ^ 2 ∧ 3072 ≤ b'P6 P n ∧ 1 ≤ dP6 P n := by sorry