Evaluation of `εAff` (round six, `epsAff_spec`)

Evaluation of εAff.

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

theorem NLogN.KFW.epsAff_spec (s : IState HS) (eR KR NR : Fin HS) (G : Ex HS → Ex HS) (e k K N B : ℕ)
    (hK : 0 < K)
    (he : s.top eR = e) (hei : s.IsInt eR) (hk : s.top NLogN.KFW.kS = k) (hki : s.IsInt NLogN.KFW.kS)
    (hKt : s.top KR = K) (hKi : s.IsInt KR) (hN : s.top NR = N) (hNi : s.IsInt NR)
    (hB : zsz (((e + k + K + N : ℕ)) : ℤ) ≤ B) (gv : ℕ → ℤ)
    (hG : ∀ (x : Ex HS) (q : ℕ), q < N → x.ok s → x.eval s = q → x.Bnd s B →
      (G x).ok s ∧ (G x).eval s = gv q ∧ (G x).Bnd s B) :
    (εAff eR KR NR G).ok s ∧
    (εAff eR KR NR G).eval s =
      (if k ≤ e ∧ (e - k) % K = 0 ∧ (e - k) / K < N then gv ((e - k) / K) else 0) ∧
    (εAff eR KR NR G).Bnd s B

Context. KFW: the exponent expressions of the uniform phase passes

The uniform phase pass phLU … εE reads, in iteration k (index on kS), the exponent εE = aE k mod 4. For the stride-K layouts of the level procedure, pos i = e - K φ(i) with φ : ι ≃ Fin N, so

aEof pos a' p = if p ≤ e ∧ K ∣ e - p ∧ (e - p)/K < N then a' (φ⁻¹ ((e-p)/K)) else 0

(aEof_equiv), which the expression εAff eR KR NR G computes from the run-time registers eR = e, KR = K, NR = N (εAff_spec), with G the exponent of a given index:

• εLit c (G = c): S_D (c = 1), ZD (c = 2), fixG (any, a' = 0 uses lit 0);
• εTab fR a (G q = a (q / f) mod 4 through a lookup list, f on fR): the node phases a' (a, c) = a_a on Fin mC × Fin (mC^k) (φ = finProdFinEquiv).

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