The Prop 18 descriptor for `n` (round six, `desc18P_run_g`)

Proved

NLogN.KFM.desc18P_run_g

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

complexity-theoryinteger-multiplicationkappa-improvement

The Prop 18 descriptor for n.

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

theorem NLogN.KFM.desc18P_run_g (dst : Fin HS) (hd : D18Ok dst) {d₀ d₁ r₀ K₀ ℓ₀ b₀ : ℕ} (hd1 : 1 ≤ d₀)
    (t : IState HS)
    (h : D18G t d₀ d₁ r₀ K₀ ℓ₀ b₀) :
    (desc18P dst).ok t ∧ (desc18P dst).run t =
      t.upd dst (ints (desc18 ((6 * b₀)) (ℓ₀) (K₀) (tsG d₀ d₁ r₀)) ++ t.G dst)

Context. Round six, chirp: the Prop 18 descriptor for any parameters

The frozen KFMSD.desc18P_run_n / desc18P_cost_n with the values of n (dP n, dpN n, rP n, KP n, ℓP n, bP n) replaced by free values d₀ d₁ r₀ K₀ ℓ₀ b₀ on the registers.

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_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false
set_option maxHeartbeats 1000000

open NLogN NLogN.KFM
open IntMul IntMul.OpenAI.Glue IntMul.OpenAI.RP NLogN.RS

Formal statement

theorem NLogN.KFM.desc18P_run_g (dst : Fin HS) (hd : D18Ok dst) {d₀ d₁ r₀ K₀ ℓ₀ b₀ : ℕ} (hd1 : 1 ≤ d₀)
    (t : IState HS)
    (h : D18G t d₀ d₁ r₀ K₀ ℓ₀ b₀) :
    (desc18P dst).ok t ∧ (desc18P dst).run t =
      t.upd dst (ints (desc18 ((6 * b₀)) (ℓ₀) (K₀) (tsG d₀ d₁ r₀)) ++ t.G dst) := 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.KFM.desc18P_run_g`, Solutions/R6ZSD.lean (lines 38–103) of the round-six development.

View graph