le_SRW (KFUU: KFU's `Φ` facts under the weaker size hypothesis)

The following holds (Lean statement, in the scope of module Solutions.KFUUWeak):

theorem NLogN.KFUU.le_SRW (d h : ℕ) (bL : ℕ → Bool) (sF : ℕ → ℕ)
    (hs : ∀ j < d, sF j ≤ 2 ^ (h + if bL j then 1 else 0)) :
    List.Forall₂ (· ≤ ·) (NLogN.KFU.shR d (NLogN.KFU.sP d sF)) (NLogN.KFU.shR d (NLogN.KFU.tP d h bL))

Context. The lemma belongs to the part KFUU: KFU's Φ facts under the weaker size hypothesis: PhiNeed only assumes s_j ≤ 2^(h + [bL j]) (the padded size tP d h bL j), not s_j ≤ 2^h. These are copies of KFU's le_SR/le_SK, phi_spec/phiInv_spec, PhiD_at/PhiInvD_at, PhiD_eq/PhiInvD_eq, PhiInvD_PhiD/PhiD_PhiInvD with that hypothesis (suffix W); the proofs only used s_j ≤ tP d h bL j.

Formalization Note. This lemma belongs to layer 5 of the Lean formalization (integer-multiplication-kappa campaign) of the OpenAI preprint Integer multiplication below $n\log n$: the uniform item-language machine (register programs over the NLogN multitape framework) assembling the Proposition 14 / Lemma 13 / Proposition 18 pieces, the resampling and chirp stages and the cost recurrences into one fixed machine, culminating in NLogN.KFTop.kappa_bound : IntMul.KappaBound (1 / 2 ^ 182) (the bound of Def_IntMul_MultitapeModel). All names refer to the definition bundles up to IntMul_Kappa_K_Defs33.