lemma12_fine_rat (KFE: fine Lemma 12, unconditional versions)

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

theorem NLogN.KFE.lemma12_fine_rat (Qc : QCircuit (ZMod 2) m W) (hm : 2 ≤ m)
    (gatesOK : ∀ g ∈ Qc.gates, g.OK)
    (route : ∀ (v : Fin W → ZMod 2) w, scalarRun Qc.gates v (Qc.ρ w) = v w)
    (unit : ∀ w, Qc.Mout (Qc.ρ w) - Qc.Min w = 1) {τ : ℝ} (hτ : 0 < τ ∧ τ < 1)
    (hs : ((frameSum (fun A : QMat m => A.rank) Qc.gates Qc.Min Qc.Mout : ℕ) : ℝ) / W <
      (m : ℝ) ^ τ) :
    ∃ T q₀ : ℕ, ∀ q, q.Prime → q₀ < q → ∃ K : ℝ, 0 ≤ K ∧
      ∀ (u : ℕ) (Pre G Suf : Shape) (Bb : ℕ), 1 ≤ u →
      (∀ a ∈ Pre, 1 ≤ a) → (∀ a ∈ G, 1 ≤ a) → (∀ a ∈ Suf, 1 ≤ a) →
      zsz ((T * (q ^ 2 * vol (binShape Pre G Suf (2 ^ u)) + 1) ^ 2 : ℕ) : ℤ) ≤ Bb → 1 ≤ Bb →
      ∀ (I : List Sym) (s : IState HS) (F : Fin HS → List ℤ) (xs : List (ZMod 2))
        (LP LG LS LU : List ℤ),
      F kP = (vol Pre : ℤ) :: LP → F kG = (vol G : ℤ) :: LG → F NLogN.KIL.kS = (vol Suf : ℤ) :: LS →
      F aU = (u : ℤ) :: LU → F 0 = enc2 xs →
      F 8 = [] → F 9 = [] → F 10 = [] → F 11 = [] → F 15 = [] → F 20 = [] → F 21 = [] →
      F 23 = [] → F 24 = [] →
      xs.length = vol (binShape Pre G Suf (2 ^ u)) →
      ∃ c : ℕ, IRuns I (progF (Qc.toCircuit 1) (edgeTplQ Qc)) (l12F q m W) (encK s F)
        (encK s (Function.update F 0 (enc2 (AModel.pull (binShape Pre G Suf (2 ^ u))
          (binShape Pre G Suf (2 ^ u)) (swapPos Pre.length (Pre.length + 1 + G.length)) 0 xs))))
        c ∧
        (c : ℝ) ≤ K * (((vol (binShape Pre G Suf (2 ^ u)) : ℝ) + 1) * (u : ℝ) ^ τ +
          ((u : ℝ) + 1) ^ (Nat.clog m (frameSum (fun A : QMat m => A.rank) Qc.gates Qc.Min Qc.Mout + 1)
            + 1) * ((Bb : ℝ) + 2) ^ 2)

Context. The lemma belongs to the part KFE: fine Lemma 12, unconditional versions.

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.