s_c / W_c ≤ m^{τ50}

s_c / W_c ≤ m^{τ50}.

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

theorem NLogN.KFM.sc_div_Wc_le :
    (P8Lift.sc : ℝ) / P8Lift.Wc ≤ ((100 ^ 3 : ℕ) : ℝ) ^ τ50

Context. The lemma belongs to the part KFM 5: the recursion exponent of complexIface is λ = τ50 = 1 - 2^{-50}: KFN.lam_complex_lt_one only gives λ = log_m max(s_c/W_c, m^{τ50}, 1) < 1. The machine budget (MACHINE-PLAN.md §5 (C)) needs λ + c < λ' with c = 2^{-56}, λ' = 1 - 2^{-54}. Here: s_c / W_c ≤ m^{τ50} (sc_div_Wc_le), hence Rb = m^{τ50} and lam_complex_eq: λ = τ50; lam_add_c_lt: λ + 2^{-56} < 1 - 2^{-54}.

Formalization Note. This lemma belongs to the item-language (IL) layer of the integer-multiplication-kappa campaign: tape-level programs (register programs over 64 item stacks of the NLogN multitape framework, definition bundles IntMul_HvdH_M_Defs1–IntMul_HvdH_M_Defs8) that implement the data-movement primitives of the OpenAI preprint Integer multiplication below $n\log n$ (field moves, row split/merge, shifts, the uniform Proposition 11 interchange, Lemma 12 with fine $O(1)$-per-element costs, Gaussian record primitives, Proposition 14 pieces) with exact list denotations from the array-model bundles IntMul_Kappa_K_Defs* and explicit cost bounds. All names refer to the definition bundles up to IntMul_Kappa_K_Defs20.