Prove2Me

AxisU6 from table facts and FineU6

Proved
IntMul.Kappa.R6.Leaf.axisU6_of_fine

by Ethan Cheung Wang · Oct 21, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theoryinteger-multiplicationturing-machines

Under the table hypotheses of LineNeed6 — namely SwapNeedτ, RowUCP, and FineU6 — the per-axis B-line interface AxisU6 P tab holds for every admissible round-six parameter record PP.

This is the B-side remaining leaf in the lineBody6_top reduction of LineNeed6 (assembled in the source by J6Seg.Ax.axisU6_of at plan ap6).

Preamble
import Definitions.Def_IntMul_Kappa_R6_Defs63

set_option autoImplicit false
set_option relaxedAutoImplicit false

open J6Seg
open IntMul.Kappa.R6
open NLogN
Formal statement
namespace IntMul.Kappa.R6.Leaf

theorem axisU6_of_fine (P : Prm) (hP : P.Ok) (tab : Fin 1 → IStmt HS 1)
    (hSw : IL.SwapNeedτ tab P.τ) (hRow : IL2.RowUCP 576 P.τ tab) (hFU : FineU6 tab) :
    AxisU6 P tab := by
  sorry

end IntMul.Kappa.R6.Leaf
Source
xuanji round-six κ development; cf. J6Seg.lineNeed6_of / jain_round6_framework_leaf

View graph