Round-six lemma `sp_hdr`

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

theorem IntMul.Kappa.R6.sp_hdr (s : IState HS) (f : Fin HS → List ℤ) (d h α p Aa Bb : ℕ)
    (l25 l33 l35 l30 : List ℤ) (h25 : f 25 = (d : ℤ) :: l25) (h33 : f 33 = (h : ℤ) :: l33)
    (h35 : f 35 = (α : ℤ) :: l35) (h30 : f 30 = (p : ℤ) :: l30) (hAa : 2 ≤ Aa)
    (hB : Aa ^ 6 < 2 ^ Bb) (hdA : d ≤ Aa) (hhA : h ≤ Aa) (hαA : α ≤ Aa) (hpA : p + 2 ≤ Aa) :
    Sp hdrP (encK s f) (encK s (update (update (update f 26
      ([((p + 2 : ℕ) : ℤ), (h : ℤ), (d : ℤ)] ++ f 26)) 27
      ([(h : ℤ), (p : ℤ), (α : ℤ), (h : ℤ), (d : ℤ)] ++ f 27)) 28
      ([(p : ℤ), (α : ℤ), (h : ℤ), (d : ℤ)] ++ f 28))) (26 * kU Bb)

Context. Round-six setup, part 7: descriptor headers and the register file

• hdrP: pushes the headers of the three descriptors (26: [p+2, h, d], 27: [K, p, α, h, d] with K = h, 28: [p, α, h, d]).
• regP: pushes the register file rS, …, rF, rPw, rOne (registers 6–16, 18, 19).

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