Closed fine oracle cost: ilCostF j V ≤ K₀ (V + W^j) (m^j)^τ + (Kb + S·Kd)(S+1)^j (Bb+2)² when S/W < m^τ

Closed fine oracle cost: ilCostF j V ≤ K₀ (V + W^j) (m^j)^τ + (Kb + S·Kd)(S+1)^j (Bb+2)² when S/W < m^τ.

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

theorem NLogN.KFD.ilCostF_le {m W S : ℕ} (K Kb Kd q : ℕ) (hm : 2 ≤ m) (hW : 1 ≤ W) {τ : ℝ}
    (hτ : 0 < τ ∧ τ < 1) (hs : (S : ℝ) / W < (m : ℝ) ^ τ) :
    ∃ K₀ : ℝ, 0 ≤ K₀ ∧ ∀ Bb j V, (ilCostF W K Kb Kd S q Bb j V : ℝ) ≤
      K₀ * ((V : ℝ) + (W : ℝ) ^ j) * ((m : ℝ) ^ j) ^ τ +
        ((Kb : ℝ) + (S : ℝ) * Kd) * ((S : ℝ) + 1) ^ j * ((Bb : ℝ) + 2) ^ 2

Context. The lemma belongs to the part KFD: closed bound of the fine Prop. 11 cost: ilCostF_le_coeff: ilCostF j V ≤ (V + W^j)·G_j + (Kb + S·Kd)·(S+1)^j·(Bb+2)² with G_{j+1} = (S/W) G_j + K(q+1) (no (Bb+2)² factor on the volume term). ilCostF_le: when S/W < m^τ, ilCostF j V ≤ K₀ (V + W^j) (m^j)^τ + (Kb + S·Kd)(S+1)^j (Bb+2)². The second term is the per-call overhead: (S+1)^j bounds the number of calls of the recursion, each paying O((Bb+2)²) for its descriptor and parameter pushes.

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_Defs18.