The chirp from Prop 18 (round six, `chirp_of_P18`)

Proved

IntMul.Kappa.R6.chirp_of_P18

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

complexity-theoryinteger-multiplicationkappa-improvement

The chirp from Prop 18 at the round-six sizes.

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

theorem IntMul.Kappa.R6.chirp_of_P18 (P : Prm) (hP : P.Ok) (tab : Fin 1 → IStmt HS 1) (H : P18Body6 P tab) :
    ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eC : Fin (7 + E)) (C₀ : ℝ) (A n₁ : ℕ),
      0 ≤ C₀ ∧
    ∀ (Q : Q6), Q.P = P → QOk Q → n₁ ≤ Q.n → ∀ (D : ℕ), Q.d = D + 1 →
    ∀ [∀ i, NeZero (Q.tB D i)],
    ∃ (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) (ζ : ℂ),
      ζ ^ Q.tB D (Fin.last D) = -1 ∧
      Phases Q.p (twX (Q.tB D) ζ) θt ∧
      Phases Q.p (fun j => (twX (Q.tB D) ζ j)⁻¹) θit ∧
      Phases Q.p (fun j => (starRingEnd ℂ) (chirp (Q.sB D) (Q.tB D) j)) at' ∧
      Phases Q.p (chirp (Q.sB D) (Q.tB D)) bt ∧
      Grid Q.p bt ∧
      ∀ Isym, chirpG6 Isym (IL.kTableP tab ext) eC cS C₀ A Q D θt θit at' bt

Context. Round six, chirp: P18Body6 → chirpG6

The frozen KFZMain.chirpNeedR_of_P18 at the round-six sizes: the chirp procedure body (KFZFull) is the own procedure of the merged table mExt4 ext₁₈ ∅ ∅ ∅ [body] in kTableP tab; the Prop 18 procedure (from P18Body6) is reached through g4₁. The descriptor stack is cS = 36. Per call M̃r = mrtCall t F G H with H the Prop 18 result, within errW6 · 2^{-p}.

chirp_of_P18: one table, entry, constants for all sizes Q of the parameters P with QOk Q: the grid tables θ̃, θ̃⁻, ã, b̃ with their Phases facts and chirpG6.

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 IntMul IntMul.Kappa IntMul.Kappa.R6
open IntMul NLogN NLogN.KIL NLogN.KFB NLogN.KFM IntMul.OpenAI.Glue IntMul.OpenAI.RCost NLogN.KFZ IntMul.OpenAI.RC IntMul.OpenAI.RT

Formal statement

theorem IntMul.Kappa.R6.chirp_of_P18 (P : Prm) (hP : P.Ok) (tab : Fin 1 → IStmt HS 1) (H : P18Body6 P tab) :
    ∃ (E : ℕ) (ext : Fin E → IStmt HS (7 + E)) (eC : Fin (7 + E)) (C₀ : ℝ) (A n₁ : ℕ),
      0 ≤ C₀ ∧
    ∀ (Q : Q6), Q.P = P → QOk Q → n₁ ≤ Q.n → ∀ (D : ℕ), Q.d = D + 1 →
    ∀ [∀ i, NeZero (Q.tB D i)],
    ∃ (θt θit at' bt : ((i : Fin (D + 1)) → ZMod (Q.tB D i)) → ℂ) (ζ : ℂ),
      ζ ^ Q.tB D (Fin.last D) = -1 ∧
      Phases Q.p (twX (Q.tB D) ζ) θt ∧
      Phases Q.p (fun j => (twX (Q.tB D) ζ j)⁻¹) θit ∧
      Phases Q.p (fun j => (starRingEnd ℂ) (chirp (Q.sB D) (Q.tB D) j)) at' ∧
      Phases Q.p (chirp (Q.sB D) (Q.tB D)) bt ∧
      Grid Q.p bt ∧
      ∀ Isym, chirpG6 Isym (IL.kTableP tab ext) eC cS C₀ A Q D θt θit at' bt := 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.chirp_of_P18`, Solutions/R6ZMain.lean (lines 36–198) of the round-six development.

View graph