Centered extraction (Lemma 17) (round six, `extract`)

Centered extraction (Lemma 17). If Z = ∑_{j<J} h_j B^j = ∑_{j<J} q_j B^j + ε B^J with B = 2H, h_j ∈ [-H, H), 0 ≤ q_j < B, then for every j ≤ J the residual identity holds, the carry is in {0,1}, and every centered residue below j equals h_k.

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

theorem Synth.extract {H : ℤ} (hH : 0 < H) {h q : ℕ → ℤ} {ε : ℤ} {J : ℕ}
    (hh : ∀ j < J, -H ≤ h j ∧ h j < H) (hq : ∀ j, 0 ≤ q j ∧ q j < 2 * H)
    (hZ : ∑ j ∈ range J, h j * (2 * H) ^ j = ∑ j ∈ range J, q j * (2 * H) ^ j + ε * (2 * H) ^ J) :
    ∀ j ≤ J, tail (2 * H) h J j = tail (2 * H) q J j + rho H q j + ε * (2 * H) ^ (J - j) ∧
      (rho H q j = 0 ∨ rho H q j = 1) ∧ ∀ k < j, cent H (q k + rho H q k) = h k

Context. §7 Lemma 17: signed packing, centered extraction, negacyclic fold, truncation

All the arithmetic content of Lemma 17, stated over ℤ (and over a coefficient model for the ring-level identification).

• Packing (gam, dig): with carry γ₀ = 0, d_j = (u_j + γ_j) mod B, γ_{j+1} = (u_j + γ_j - d_j)/B; pack_digit, pack_carry (γ_j ∈ {-1,0} when |u_j| < B), pack_telescope (∑ u_j B^j = ∑ d_j B^j + γ_r B^r), pack_sign (γ_r = -1 ↔ A_u < 0).
• pack_bound: |u_j| ≤ c, 2c < B give 2|A_u| < B^r.
• cnv (ordinary product coefficients), eval_mul_cnv (A_a A_c = ∑_{j<2r} h_j B^j), abs_cnv_le and coeff_bound31 (|h_j| ≤ r 2^{2p} < 2^{3p}, 2·2^{3p} < B₀ = 2^{4p}).
• twos_complement_exists: a fixed-width signed block representation Z = ∑ q_j B^j + ε B^J.
• Extraction (cent, rho): extract proves the residual identity, ρ_j ∈ {0,1}, exact recovery ĥ_j = h_j, and ρ_J + ε = 0; kron_recover is the instance of Lemma 17.
• Negacyclic fold: fold_formula, co_mul and co_mul_gauss (the Gaussian numerators of f g are (ac - be) + i(ae + bc) folded modulo y^r + 1).
• Truncation: truncNum_div (trunc₀(H / 2^{p+ℓ}) is H.tdiv 2^{p+ℓ}), Qp_normalized.
• Scaling by appending zeros: append_zeros.

Formalization Note. Part of the Lean formalization of the round-six κ-improvement (integer-multiplication-kappa campaign, target IntMul.Kappa.jain_round6_framework). The statement is copied verbatim from the Lean development; the platform node carries the same declaration name. Definitions it mentions live in the IntMul_Kappa_R6_Defs* bundles (on top of the published κ bundles IntMul_Kappa_K_Defs*).