One phase on a state whose `t`-digits are `≤ R - 2` and whose segments satisfy `1 ≤ v`, `v + 2R < W` (`phInv_spec`)

One phase on a state whose t-digits are ≤ R - 2 and whose segments satisfy 1 ≤ v, v + 2R < W: t, u unchanged, segment v ↦ v + z (1 - 2 a).

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

theorem IntMul.Kappa.R6.IL2C.phInv_spec (hK : 1 ≤ K) (hG : 1 ≤ G) (hL : ρ + n * K ≤ L) {t u y : ℕ}
    (hb : Box G n L ⟨t, u, y⟩) (ht : ∀ s < n, cdg G s t + 2 ≤ 2 ^ G)
    (hv : ∀ s < n, 1 ≤ IntMul.Kappa.R6.IL2C.seg K ρ s y ∧ IntMul.Kappa.R6.IL2C.seg K ρ s y + 2 * 2 ^ G < 2 ^ K) :
    ∃ y', phInv K ρ G n L ⟨t, u, y⟩ = ⟨t, u, y'⟩ ∧ y' < 2 ^ L ∧ y' % 2 ^ ρ = y % 2 ^ ρ ∧
      y' / 2 ^ ρ / (2 ^ K) ^ n = y / 2 ^ ρ / (2 ^ K) ^ n ∧
      ∀ s < n, (IntMul.Kappa.R6.IL2C.seg K ρ s y' : ℤ) = IntMul.Kappa.R6.IL2C.seg K ρ s y +
        ((cdg G s u % 2 : ℕ) : ℤ) * (1 - 2 * ((ybit K ρ s y : ℕ) : ℤ))

Context. Round six, compact controls (I2C): the value-level mechanism

Colkitt's compact dirty controls, uniform variant (see jain6/compact/DESIGN.md). The state of one record is (t, u, y) (the temporary T, the control U, the target slot Y); the source slot x is a parameter. Radices: W = 2^K (slot segments), R = 2^G (compact digits); n low selected positions j_s = ρ + s K.

• dgt W s x = x / W^s % W; digits_add: digit-wise addition without carries; eq_of_digits: equal low digits and equal high part give equal numbers.
• segSum tf ru rv rw w0 u v n = Σ_{s<n} w0 rw^s tf (u / ru^s) (v / rv^s) (the register loop).
• The offsets oA (Y += Σ 2 z_s t_s 2^{j_s}), oB (Y += Σ z_s (1 - 2 t_s) 2^{j_s}), oS (packed selected bits), oC (Σ (y_s xor z_s) R^s), oT (the ideal toggle).
• The pull maps rT, rU, rY, the inverse phase phInv and the whole pull composite Psi.
• Psi_good: on a good state Psi is the ideal map (toggle the n low selected bits of y by those of x); Psi_bij-type facts are proved at rank level.

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*).