Lemma 16 ↔ Proposition 14 (round six, `paper_round_layer`)

Lemma 16 ↔ Proposition 14. For a slot b ≤ h < b + qK, every axis takes part in round h, and the round's selected bits act exactly as layerSel (2^A) K D (2^B) ρ: bit ρ = (h-b) mod K of each of the D consecutive K-bit chunks of group j₀ (tgt_slot).

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

theorem GlueLayout.paper_round_layer (hK : 0 < K) (hℓ : 1 ≤ ℓ) {h : ℕ} (hb : bb ℓ K ≤ h)
    (hh : h < bb ℓ K + qq ℓ K * K) (M : M2) {X : Type*} [AddCommMonoid X] [Module ℂ X]
    (xs : List X) :
    selOp (paperSel D ℓ K long hK hℓ h) (tens M) xs =
      selOp (layerSel (2 ^ preA D ℓ K long h) K D (2 ^ sufB D ℓ K h) (rhoOf ℓ K h)
        (rhoOf_lt ℓ K hK h)) (tens M) xs

Context. Glue 2a: the paper's layout as a CoordLayout, its selected bits, and the bridge to layerSel

• §0 bit arithmetic: getBit_bitsum, bitsum_update (binary digit sums), getD_decode (a digit of decode), getD_decode_binSh (bits of a binary address).
• §1 PosData/posSel: selected bits of a binary address given by bit positions; selOp_transport: two selected-bit structures related by an address map preserving the linear index give the same selOp for every tensor kernel.
• §2 slotLayout: a slot arrangement arr (a list of slot names nm i h covering every slot h < a i exactly once) is a CoordLayout (binSh |arr|) a; slotSel (round h, axes P) is SelCompat with it (slot_compat).
• §3 chunk_bridge: if the selected positions are A + iK + (K-1-ρ) in a binary address of length A + DK + B, the selected-bit operator is layerSel (2^A) K D (2^B) ρ of §5.
• §4 the paper's layout tgtL (SynthLayoutPaper): paperLayout, paperSel, synth_forward_paper (§6.1 on the concrete layout: the rounds implement B F^-), and paper_round_layer (for every slot b ≤ h < b + qK the round's simultaneous layer is exactly Proposition 14's layerH (2^A) K D (2^B) ρ with ρ = (h-b) mod K, via tgt_slot).

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