Fine-bit exposure at every admissible round-six parameter record

Proved

IntMul.Kappa.R6.Leaf.fineNeed6_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 fine-bit exposure interface FineNeed6 P 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 fineNeed6_all (P : Prm) (hP : P.Ok) : FineNeed6 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).