AxJ eventually on every round-six axis

Proved

J6Seg.Side.axJ_ev

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplication

For every admissible round-six parameter record $P$ there exists a threshold $n_1$ such that for all $n\ge n_1$ and every admissible source list, every axis carries an AxJ witness (side bounds, segment regularity, and window hypotheses).

This is the numeric input to jBudget6_all.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false

open J6Seg J6Seg.Side
open IntMul.Kappa.R6

Formal statement

namespace J6Seg.Side

theorem axJ_ev (P : IntMul.Kappa.R6.Prm) (hP : P.Ok) :
    ∃ n₁ : ℕ, ∀ n, n₁ ≤ n → ∀ src : ℕ → ℕ,
      IntMul.Kappa.R6.SrcOK6 P n src → ∀ D : ℕ, IntMul.Kappa.R6.dP6 P n = D + 1 →
      ∀ k ≤ D, AxJ P n src D k := by
  sorry

end J6Seg.Side

Source

xuanji round-six κ; Solutions.J6SegJCost3

View graph