Symmetry of hook+column coefficients in iterated plethysms

A hook+column partition (α,2^β,1^γ) has a first part α, followed by β parts equal to two and γ parts equal to one. Let g be a homogeneous rational symmetric function of degree d≥1, let a≥2, and put f=g[hₐ]. We prove that, for each fixed γ, the Schur coefficients of f at these partitions, listed by β from $0$ to d-1-γ, read the same forwards and backwards, zero entries included, and that they vanish for larger β. Consequently, every iterated plethysm of complete homogeneous functions has symmetric hook+column sequences, answering Question 1 of Gutiérrez and Rosas. They gave explicit formulas for two three-factor families and proved that the second symmetric and exterior plethysms s₍₂₎[f] and s(1,1)[f] of a Schur-positive f preserve flip-symmetry, a stronger form of this symmetry; Langley and Remmel gave the underlying two-factor formula. We extend the symmetry to every number of factors and every positive index, and retain the zero entries. The argument uses Gutiérrez and Rosas's specialization at the signed alphabet $1-x-y$. After division by $(1-x)(1-y)$, replacing x and y by their reciprocals gives the coefficient identity. A Lean formalization proves the result from power-sum, Newton, and Jacobi–Trudi definitions, including the existence and uniqueness of Schur expansions. This work has not yet been reviewed by experts. The proofs, the Lean formalization and the text were produced by AI models (from OpenAI and Anthropic), working under the author's direction. Computer-assisted; not yet reviewed by experts. Produced by AI models under the author's direction.