λ + c < λ': τ50 + 2^{-56} < 1 - 2^{-54}

λ + c < λ': τ50 + 2^{-56} < 1 - 2^{-54}.

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

theorem NLogN.KFM.lam_add_c_lt :
    Real.logb ((100 ^ 3 : ℕ) : ℝ) (Rb P8Lift.sc P8Lift.Wc (100 ^ 3) τ50) + (2 : ℝ)⁻¹ ^ 56 <
      1 - (2 : ℝ)⁻¹ ^ 54

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.