Prove2Me

AxBudget6 at the concrete plan ap6

Proved
J6Seg.ChB.axBudget6_ap6

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

complexity-theoryinteger-multiplication

For every admissible round-six parameter record PP, the axis budget interface AxBudget6 P ap6 holds at the concrete round-six axis plan ap6.

This is the hBud leaf used by J6Seg.Ax.axisU6_of in the B-line assembly.

Preamble
import Definitions.Def_IntMul_Kappa_R6_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false

open J6Seg J6Seg.ChB
open IntMul.Kappa.R6
Formal statement
namespace J6Seg.ChB

theorem axBudget6_ap6 (P : IntMul.Kappa.R6.Prm) (hP : P.Ok) :
    AxBudget6 P IntMul.Kappa.R6.ap6 := by
  sorry

end J6Seg.ChB
Source
xuanji round-six κ; Solutions.J6SegAxBud9

View graph