Soundness of the readout check (round six, `rdS_sound`)

Soundness of the readout check.

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

theorem IntMul.Kappa.R6.Cx.NetMask.rdS_sound (t : BT) (C : ℕ → ℕ → ℕ) (hE : Enc t C) (S : ℕ) (L : List (ℕ × ℤ))
    (h : rdS t S L = true) (u : ℕ) :
    (L.map fun p => p.2 * (C p.1 u : ℤ)).sum = if u = S then 2 else 0

Context. The scalar identity of the local program by a kernel mask simulation

The gate DAG L of the local program is run on spread inputs: slot src t receives 256^t (the coefficient vector e_t in base 256), each gate op a_q += a_r adds the encoded vectors, and every intermediate vector is checked to have digits in {0, 1} (Nat.land v LO = v). The readout check compares ∑ k · a with 2 · 256^S for every triple S.

• vget / vset: one value per leaf of a binary tree (recursor form, raw primitives).
• enc f = ∑_{t < NV} f t · 256^t; simK_sound: the kernel run encodes runP ops C, the run on coefficient vectors, and keeps all digits in {0, 1}.
• readChk_sound: the readout identity on coefficient vectors.

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