Common offset (round six, `tgt_slot`)

Common offset. In the target order, slot (i, h) with b ≤ h < b + qK sits in the i-th chunk of chunk group j = ⌊(qK-1-(h-b))/K⌋, at offset ρ = (h-b) mod K from the least significant end of that chunk (position K-1-ρ inside it).

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

theorem Synth.tgt_slot (hK : 0 < K) (i : Fin D) {h : ℕ} (hb : bb ℓ K ≤ h) (hh : h < bb ℓ K + qq ℓ K * K) :
    let e := qq ℓ K * K - 1 - (h - bb ℓ K)
    (tgtL D ℓ K long).getD ((lstL D ℓ K long).length + ((e / K) * D + i) * K + (e % K)) 0 =
      nm D i h ∧ K - 1 - e % K = (h - bb ℓ K) % K

Context. §6.2 Lemma 16: the paper's layout L

Axes i < D have a_i = ℓ (long) or ℓ - 1 (short) address bits; slot h of axis i is named nm i h = h·D + i. With b = (ℓ-1) mod K and q = ⌊(ℓ-1)/K⌋:

• the prefix list Lst: the top slots (i, ℓ-1) of the long axes (increasing i), then (i, h) for h = b-1, …, 0 and, within each h, increasing i;
• after the prefix moves every axis keeps the qK slots h = ℓ-2, …, b (restA), which are q consecutive K-bit chunks (chunk i j, numbered from the top);
• the target order tgt = Lst ++ (chunks in chunk-major order).

paper_layout: L is reached by |Lst| ≤ D(b+1) single moves and at most Dq - 1 chunk exchanges, and its array denotation is the pull by relabel init tgt. tgt_slot: in the target, slot (i, h) (b ≤ h ≤ ℓ-2) lies in chunk i of chunk group j = ⌊(qK-1-(h-b))/K⌋, at offset (h - b) mod K from the least significant end — the common offset used by the simultaneous layer (Proposition 14).

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