Round-six lemma `opK_CH`

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 R6Pk.R6CxNetG):

theorem IntMul.Kappa.R6.Cx.NetG.opK_CH : ∀ o ∈ progOps CH, OpK o

Context. The round-six complex network in the item-language gate class (GClassH)

R6CxNetFinal.net uses mergedChunk (an opaque Classical.choose of merge_chunk) for its frame changes; its steps cannot be inspected. netG is the same network with every merged chunk replaced by the explicit chunkH (row additions, one child, row additions) chosen from merge_identity: same denotation, same child widths. Its only gates are the chunk gates GOp.mat:

• z_d += (k/2) z_s with d ≠ s (all local ops, C1, C2): |k| KFG atoms (d, s, sign k, h = 1);
• z_X += -2 z_X (C3): the ±1 diagonal -1 at X.

cxNetR6G : ∃ T (J : Prop8IfaceH 207387136 T 576 Jain.cxR6) A, GClassH J A.

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