ChunkBudget6 for every ChunkPlan6 / ChunkPlanB axis plan

Proved

J6Seg.ChB.chunkBudget6_all

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

complexity-theoryinteger-multiplicationround-six

Chunk-pass budget for every plan with ChunkPlan6 and ChunkPlanB.

For every $P.\mathrm{Ok}$ and every axis plan $ap$ carrying both chunk-plan interfaces, ChunkBudget6 P ap holds.

Third half of axBudget6_of, used at ap6 once ChunkPlanB ap6 is discharged by decide.

Preamble

import Definitions.Def_IntMul_Kappa_R6_Defs70

set_option autoImplicit false
set_option relaxedAutoImplicit false

Formal statement

namespace J6Seg.ChB

open J6Seg J6Seg.AxCh
open IntMul.Kappa.R6

theorem chunkBudget6_all (P : Prm) (hP : P.Ok) (ap : AxPlan6)
    (hc : ChunkPlan6 ap) (hcb : ChunkPlanB ap) : ChunkBudget6 P ap := by
  sorry

end J6Seg.ChB

Source

xuanji round-six (Solutions.J6SegAxBud / chunk budget); feeds axBudget6_of / axBudget6_ap6

View graph