Round-six lemma `twoAtanP_cost`

Proved

NLogN.twoAtanP_cost

by xuanji · Oct 20, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationkappa-improvement

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

The following holds (Lean statement, in the scope of module NLogN.HNumPi):

theorem NLogN.twoAtanP_cost (x₁ x₂ : ℕ) (σ c₁ c₂ : ℤ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂) (hσ : |σ| = 1)
    (hc₁ : |c₁| ≤ 16) (hc₂ : |c₂| ≤ 16) (n : ℕ)
    (s : IState HS) (L3 : List Item) (h3 : s.G 3 = .int n :: L3) :
    (twoAtanP x₁ x₂ σ c₁ c₂).cost s ≤
      10 ^ 11 * (2 * n + 11) * (atanB x₁ (2 * n + 9) (2 * n + 9) +
        atanB x₂ (2 * n + 9) (2 * n + 9) + 6) ^ 2

Context. piBits and log2Bits as register programs

Input n on register 3; the result is pushed on register 4. Uses registers 0, 1, 2, 40 … 47.

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

Preamble

-- 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

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN
open IntMul NLogN.RS

Formal statement

theorem NLogN.twoAtanP_cost (x₁ x₂ : ℕ) (σ c₁ c₂ : ℤ) (hx₁ : 0 < x₁) (hx₂ : 0 < x₂) (hσ : |σ| = 1)
    (hc₁ : |c₁| ≤ 16) (hc₂ : |c₂| ≤ 16) (n : ℕ)
    (s : IState HS) (L3 : List Item) (h3 : s.G 3 = .int n :: L3) :
    (twoAtanP x₁ x₂ σ c₁ c₂).cost s ≤
      10 ^ 11 * (2 * n + 11) * (atanB x₁ (2 * n + 9) (2 * n + 9) +
        atanB x₂ (2 * n + 9) (2 * n + 9) + 6) ^ 2 := by sorry

Source

S. Jain, round-six networks for the integer-multiplication κ-improvement campaign (https://github.com/Swapnil-jain/integer-mult-kappa, commit 5868dc7) and D. Colkitt, integer-mult-bounds (https://github.com/CrocSwap/integer-mult-bounds); target `IntMul.Kappa.jain_round6_framework`. Lean declaration `NLogN.twoAtanP_cost`, Solutions/HNumPi.lean (lines 143–236) of the round-six development.

View graph