Magnitudes of polynomial expressions (round six, `mg_le_dg`)

Proved

J6Seg.PreT.mg_le_dg

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

complexity-theoryinteger-multiplicationkappa-improvement

Magnitudes of polynomial expressions.

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

theorem J6Seg.PreT.mg_le_dg {V : Fin HS → ℕ} {A : ℕ} (hV : ∀ j, V j ≤ 2 ^ A) (hA : 2 ≤ A) :
    ∀ e : Ex HS, Poly e = true → mg V e ≤ 2 ^ (A * J6Seg.PreT.dg e)

Context. B-line IL, pre-tables (B5), part 4: polynomial expressions and the push loop

Poly e: no pow2/shl, literals of absolute value ≤ 4; dg e its degree; mg_le_dg: with every register value ≤ 2^A (A ≥ 2), mg e ≤ 2^(A·dg e). Every expression of the pre-table loops is polynomial (the powers 2^P, 2^{P+1} sit in registers 9, 10), so all cost conditions reduce to dg e ≤ D (by decide) and one uniform width B = A·D + 1.
pushLoop: a counted loop whose body pushes f k onto O leaves rv f N ++ O.

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_R6_Defs65

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open J6Seg J6Seg.PreT
open IntMul NLogN NLogN.KIL NLogN.RS

Formal statement

theorem J6Seg.PreT.mg_le_dg {V : Fin HS → ℕ} {A : ℕ} (hV : ∀ j, V j ≤ 2 ^ A) (hA : 2 ≤ A) :
    ∀ e : Ex HS, Poly e = true → mg V e ≤ 2 ^ (A * J6Seg.PreT.dg e) := 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 `J6Seg.PreT.mg_le_dg`, Solutions/J6SegILPre4.lean (lines 53–108) of the round-six development.

View graph