Round-six lemma `agree_sigmaM`

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.KFX6Run):

theorem NLogN.KFX.agree_sigmaM {t : IState HS} {vW vNt vFa vFb vQ vB vR2 vGx vN0 vN1 vN2 vN3 vA vK2 vF vK : ℤ}
    (h1 : ∃ L, t.G mW = .int vW :: L) (h2 : ∃ L, t.G mNt = .int vNt :: L)
    (h3 : ∃ L, t.G mFa = .int vFa :: L) (h4 : ∃ L, t.G mFb = .int vFb :: L)
    (h5 : ∃ L, t.G mQ = .int vQ :: L) (h6 : ∃ L, t.G mB = .int vB :: L)
    (h7 : ∃ L, t.G mR2 = .int vR2 :: L) (h8 : ∃ L, t.G mGx = .int vGx :: L)
    (h9 : ∃ L, t.G mN0 = .int vN0 :: L) (h10 : ∃ L, t.G mN1 = .int vN1 :: L)
    (h11 : ∃ L, t.G mN2 = .int vN2 :: L) (h12 : ∃ L, t.G mN3 = .int vN3 :: L)
    (h13 : ∃ L, t.G mA = .int vA :: L) (h14 : ∃ L, t.G mK2 = .int vK2 :: L)
    (h15 : ∃ L, t.G mF = .int vF :: L) (h16 : ∃ L, t.G mK = .int vK :: L) :
    Agree (σM vW vNt vFa vFb vQ vB vR2 vGx vN0 vN1 vN2 vN3 vA vK2 vF vK) t

Context. KFX §6: the bit-length loop and the run of the uniform row addition

loopZ computes A = zsz V on stack 48 by halving V (pushed on stack 14) until it is 0. rowCodeU q = withPushI hdrL (zB (l13U q)) pushes the master registers computed from the parameter registers (hdrL), runs loopZ, then l13U q.

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