`Φ` as a padded array (round six, `phiD_pad`)

Φ as a padded array.

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

theorem NLogN.KFM.phiD_pad (hsw : ∀ j < d, sF j ≤ tP d h bL j) (xs : List ℤ) {zs : List GI}
    (hz : gflat zs = PhiD h d bL sF μ xs) :
    haveI := sBox_ne sF μ H
    zs.length = (List.ofFn (tBox d h bL)).prod ∧ PadZ (sBox d sF) (tBox d h bL) zs ∧
    ∀ k : (i : Fin d) → ZMod (sBox d sF i),
      zs.getD (encode (List.ofFn (tBox d h bL)) (kL k)) 0 =
        (xs.getD (2 * ((eB sF μ H).symm k).val) 0, xs.getD (2 * ((eB sF μ H).symm k).val + 1) 0)

Context. KFM: Φ / Φ⁻¹ with s_j ≤ t_j, and as arrays of the chain

KFU states the pointwise denotations of Φ/Φ⁻¹ under s_j ≤ 2^h; the parameters have s_j ≤ t_j = 2^{h+b_j} (PhiNeed, as corrected). The proofs only use sP ≤ tP:

• sP_le_tPW, le_SRW, PhiD_atW, PhiInvD_atW, PhiD_eqW (copies with the weak hypothesis hsw : ∀ j < d, sF j ≤ tP d h bL j).

As arrays of the chain (box t_i = tP d h bL i, source s_i = sF i, last axis = component):

• encode_snoc2: enc (sh ++ [2]) (v ++ [c]) = 2·enc sh v + c.
• pairL ys: the Gaussian items of an integer list; gflat (pairL ys) = ys for even length.
• phiD_pad: pairL (PhiD xs) vanishes off the source points (PadZ) and holds the item (xs[2κ], xs[2κ+1]), κ = (Φ⁻¹ k).val, at source point k.
• phiInvD_read: (PhiInvD (gflat ws))[2m + c] is component c of ws at the point Φ(m).

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