PreA6 from NumA6 numeric facts

Proved

J6Seg.ATab.preA6_of_num

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

complexity-theoryinteger-multiplicationround-six

A-axis B4 set-up from numeric facts.

If the numeric interface NumA6 P pkA pkC bA bC holds, then for every instruction table the relocated native pair natUp / tearP witnesses PreA6 P pkA pkC bA bC tab.

This is the missing bridge between the proved J6Seg.ATab.numA6 and the Open leaf J6Seg.ATab.preA6 used by ail6s_of_fine.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs69

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace J6Seg.ATab

open J6Seg
open IntMul.Kappa.R6
open NLogN

theorem preA6_of_num {P : Prm} {pkA pkC bA bC : ℕ} (h : NumA6 P pkA pkC bA bC)
    (tab : Fin 1 → IStmt HS 1) : PreA6 P pkA pkC bA bC tab := by
  sorry

end J6Seg.ATab

Source

xuanji round-six (Solutions.J6AILTab11 preA6_of_num); uses Proved setup_of_native, natUp_sp, tearP_sp; feeds preA6

View graph