Prove2Me

AIL6s from table facts and FineU6

Proved
IntMul.Kappa.R6.Leaf.ail6s_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 segmented A-line interface AIL6s P tab holds for every admissible round-six parameter record PP.

This is the A-side remaining leaf in the lineBody6_top reduction of LineNeed6 (via J6Seg.AIL6s_of_axis from AxisUA6 and PipeGBA6).

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 ail6s_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) :
    AIL6s P tab := by
  sorry

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

View graph