CRT reversal interface CrtNeed6 at every admissible round-six parameter record

For every round-six parameter record $P$ with $P.\mathrm{Ok}$, the interface CrtNeed6 P holds: for every one-entry table tab that provides the bit network's swap procedure (IL.SwapNeedτ tab P.τ) and the compact-controls row addition (IL2.RowUCP 576 P.τ tab), there is an extension of the IL table with entry points $e_F,e_B$ implementing the maps $\Phi$ and $\Phi^{-1}$ of the CRT step (§9.3; KFU.PhiD/KFU.PhiInvD between digits in the k-order source shape and the padded reversed box) on stack 0, with descriptor descPhi6 on a stack $d_S\neq 0$, all other managed stacks empty and the unmanaged part preserved, for all sizes $n\ge n_1$ and valid sources (SrcOK6), at cost at most $C_0\,\mathrm{cU6}(P,n,A)$. The CRT axis reversal uses $3\ell$ permuted selected-bit additions with compact controls (cost row $\ell(d\ln p)^\tau$); the prefix moves and padding cost $O(Vd)$.

In Lean:

theorem IntMul.Kappa.R6.crtNeed6_all : ∀ P : Prm, P.Ok → CrtNeed6 P

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).