Gaussian line maps at every admissible round-six parameter record

Proved

IntMul.Kappa.R6.Leaf.lineNeed6_all

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

complexity-theoryinteger-multiplicationturing-machines

For every admissible round-six parameter record $P$ , the line-map interface LineNeed6 P (segmented exact inverse, Gaussian line maps) of xuanji's round-six machine holds.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs16

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace IntMul.Kappa.R6.Leaf

theorem lineNeed6_all (P : Prm) (hP : P.Ok) : LineNeed6 P := by
  sorry

end IntMul.Kappa.R6.Leaf

Source

xuanji's round-six development on Prove2me (Def_IntMul_Kappa_R6_Defs1, Defs16), Jain round seven data (Def_IntMul_KappaJainData).

View graph