Round-six lemma `retChk_ok`

An auxiliary lemma of the round-six development, published as a separate node because its proof is long or shared.

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

theorem IntMul.Kappa.R6.Bit.retChk_ok : retChk = true

Context. Round six, bit network: the scalar effect of one invocation

The gate lists of the two stage words (G1, G2) act on local wires (inputs x, targets y, slots, temporaries) of any module of characteristic two. With the temporaries starting at 0: the inputs and slots are unchanged and the targets receive the inputs, y_T ← y_T + x_T.

The proof splits the start values into the input part and the rest. On the rest, both read blocks add the same reads of the producer values, which cancel. On the inputs, the producer computes the node values (prod_vals) and the reads give back x_T (reads_eq).

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