rootP cost: ≤ (v+1)(m+3)·10^9·(Bv v + m + 2)²

rootP cost: ≤ (v+1)(m+3)·10^9·(Bv v + m + 2)².

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

theorem NLogN.KFM.rootP_cost (m : ℕ) (rv rd : Fin HS) (h : RootRegs rv rd) (s : IState HS) (v : ℕ)
    (LV : List Item) (hV : s.G rv = .int (v : ℤ) :: LV) :
    (rootP m rv rd).cost s ≤ (v + 1) * (m + 3) * 10 ^ 9 * (Bv v + m + 2) ^ 2

Context. The lemma belongs to the part KFM S1: integer roots by counting (setup of d = ⌊b^{2^{-75}}⌋ and K = ⌊d^{2^{-56}}⌋): rootP m rv rd pushes onto rd the number of x ∈ [1, v] with x^{2^m} ≤ v, where v ≥ 1 is the top of rv. Each test makes m saturated squarings y ↦ min(y², v+1) (m is a literal, a true constant: 75 or 56), so every value has O(log v) bits. The predicate is downward closed, so the count is the largest such x (count_eq_findGreatest), i.e. the integer 2^m-th root of v.

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