Round-six lemma `depH_le_log`

Proved

IntMul.Kappa.R6.IL.depH_le_log

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

complexity-theoryinteger-multiplicationkappa-improvement

depH m e ≤ log e / log (m / (m - 1)) + 1: every level shrinks the width by (m-1)/m.

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

theorem IntMul.Kappa.R6.IL.depH_le_log {m : ℕ} (hm : 2 ≤ m) : ∀ e : ℕ, 1 ≤ e →
    (Bit.depH m e : ℝ) ≤ Real.log e / Real.log ((m : ℝ) / ((m : ℝ) - 1)) + 1

Context. Round six, item language: the item-language Prop. 11 interface for a bit network

depH_le_log, depH_pow_le: the recursion depth of progH is logarithmic; at the widths m ^ k it is ≤ cW k.
ilCostR, ILProp11 tab C q T₀ c₁ K₁ K₂: at every level k (width m ^ k), with the KIL5 calling convention DescIn, the procedure tab 0 computes progH C q (m ^ k) on the bit stream at cost ⌈K₁ costH C (m^k) V + K₂ (m^k + 1)^c₁ (Bb + 2)²⌉.
ilProp11_of_net (in R6ILProp): the item-language Prop. 11 program for a round-six network.

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_MachineRef
import Definitions.Def_IntMul_KappaFramework
import Definitions.Def_IntMul_Kappa_R6_Defs4

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.RS NLogN.KIL NLogN.KFD AModel AModelL12 Finset

Formal statement

theorem IntMul.Kappa.R6.IL.depH_le_log {m : ℕ} (hm : 2 ≤ m) : ∀ e : ℕ, 1 ≤ e →
    (Bit.depH m e : ℝ) ≤ Real.log e / Real.log ((m : ℝ) / ((m : ℝ) - 1)) + 1 := 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 `IntMul.Kappa.R6.IL.depH_le_log`, Solutions/R6ILSpec.lean (lines 27–70) of the round-six development.

View graph