[proofplan] We use Fomin growth diagrams for the row-insertion Robinson-Schensted correspondence. The local growth rule determines every partition in the grid from the southwest boundary and the permutation matrix, and the northeast boundary chains encode the insertion and recording tableaux. Rotating the growth diagram by $180^\circ$ changes the permutation matrix of $\pi$ into the permutation matrix of the reverse-complement $\pi^\vee$, while the reversed local rule changes each boundary tableau into its Schützenberger evacuation. Since the same rotation applied twice is the identity, evacuation is an involution. [/proofplan]

[step:Encode the permutation by its growth diagram] Let $\Lambda$ denote the Young lattice, whose elements are partitions and whose cover relation is addition of one box. For the permutation $\pi=\pi_1\cdots\pi_n$, define the permutation matrix set \begin{align*} M_\pi := \{(i,\pi_i):1\le i\le n\}\subset \{1,\dots,n\}\times\{1,\dots,n\}. \end{align*} A Fomin growth diagram for $\pi$ is an assignment $\Gamma_\pi:\{0,\dots,n\}\times\{0,\dots,n\}\to \Lambda$ with empty partitions on the south and west boundaries, \begin{align*} \Gamma_\pi(i,0)=\varnothing,\qquad \Gamma_\pi(0,j)=\varnothing, \end{align*} and with each unit square determined by the Fomin local rule from the three southwest-corner partitions and whether the square contains a mark of $M_\pi$. By the growth-diagram convention fixed in the theorem statement, equivalently the row-insertion [Robinson-Schensted-Knuth bijection theorem](/theorems/8435) in this convention, the north boundary chain \begin{align*}\varnothing=\Gamma_\pi(0,n)\subset \Gamma_\pi(1,n)\subset \cdots \subset \Gamma_\pi(n,n)\end{align*} encodes the recording tableau $Q(\pi)$, while the east boundary chain \begin{align*}\varnothing=\Gamma_\pi(n,0)\subset \Gamma_\pi(n,1)\subset \cdots \subset \Gamma_\pi(n,n)\end{align*} encodes the insertion tableau $P(\pi)$. More explicitly, if a saturated chain of partitions \begin{align*} \varnothing=\lambda_0\subset\lambda_1\subset\cdots\subset\lambda_n \end{align*} has $|\lambda_k|=k$ for every $k$, then it encodes the standard tableau whose entry $k$ is placed in the unique box of $\lambda_k\setminus\lambda_{k-1}$. [/step]

[step:Rotate the growth diagram to obtain the reverse-complement permutation]Define the rotated labelled square $\widetilde{\Gamma}_\pi:\{0,\dots,n\}\times\{0,\dots,n\}\to\Lambda$ by \begin{align*} \widetilde{\Gamma}_\pi(i,j)=\Gamma_\pi(n-i,n-j) \end{align*} for all $0\le i,j\le n$, with the local rule read in the reverse direction. This rotated labelled square is not being asserted to have empty south and west boundary. Rather, this is exactly the square-reversal theorem assumed in the formalized statement: for a finite empty-boundary permutation growth diagram, rotating the mark set by $180^\circ$ and then forming the ordinary empty-south-and-west-boundary growth diagram for the rotated mark set gives northeast boundary tableaux equal to the Schützenberger evacuations of the original northeast boundary tableaux. The mark $(i,\pi_i)\in M_\pi$ is sent by the $180^\circ$ rotation of the $n\times n$ grid to \begin{align*} (n+1-i,n+1-\pi_i). \end{align*} Set $k=n+1-i$. Then this rotated mark is \begin{align*} (k,n+1-\pi_{n+1-k})=(k,\pi^\vee_k). \end{align*} Therefore the rotated mark set is exactly $M_{\pi^\vee}$. Since the Fomin local growth rule is reversible, Fomin's reversal theorem applies to the rotated labelled square $\widetilde{\Gamma}_\pi$: the empty-boundary growth diagram for $\pi^\vee$ has north and east boundary chains equal to the evacuated boundary chains of $\Gamma_\pi$.[/step]

[guided]The point of using growth diagrams is that RSK becomes a local rule on a square grid. We place a mark in square $(i,\pi_i)$ for each letter of the permutation. Rotating the whole square by $180^\circ$ sends the square indexed by $(i,\pi_i)$ to the square indexed by \begin{align*} (n+1-i,n+1-\pi_i). \end{align*} To identify this with the permutation matrix of $\pi^\vee$, define $k:=n+1-i$. Then $i=n+1-k$, so the second coordinate becomes \begin{align*} n+1-\pi_i = n+1-\pi_{n+1-k}=\pi^\vee_k. \end{align*} Thus every rotated mark has the form $(k,\pi^\vee_k)$, and every mark of $M_{\pi^\vee}$ arises in this way from the unique index $i=n+1-k$. Hence the rotated permutation matrix is exactly the permutation matrix of the reverse-complement permutation. We also need the local rule to remain valid after rotation. This is precisely the reversibility property of Fomin's local growth rule: from any three corners of a unit square and the mark/no-mark datum, the fourth corner is uniquely determined. The square-reversal hypothesis in the theorem statement applies because $\Gamma_\pi$ is a finite permutation growth diagram with empty south and west boundaries, saturated north and east boundary chains, and mark set $M_\pi$. It says that after rotating the mark set by $180^\circ$ and forming the ordinary empty-south-and-west-boundary growth diagram for the rotated mark set, the north boundary tableau is the evacuation of the original north boundary tableau and the east boundary tableau is the evacuation of the original east boundary tableau. Since the rotated mark set is $M_{\pi^\vee}$, Fomin's reversal theorem identifies the ordinary empty-boundary growth diagram for $\pi^\vee$ with the evacuated north and east boundary chains of $\Gamma_\pi$.[/guided]

[step:Identify the rotated boundary chains with evacuation] We use Fomin's growth-diagram characterization of $\operatorname{evac}_n$ stated in the hypotheses. If a standard tableau $T$ with entries $\{1,\dots,n\}$ is encoded by a saturated Young-lattice chain \begin{align*} \varnothing=\lambda_0\subset\lambda_1\subset\cdots\subset\lambda_n, \end{align*} then $\operatorname{evac}_n(T)$ is encoded by the opposite boundary chain in the triangular evacuation growth diagram determined by the reversible Fomin local rule. The hypotheses are satisfied here because the north and east RSK boundary chains above are saturated chains in the Young lattice beginning at $\varnothing$ and ending at the common shape of $P(\pi)$ and $Q(\pi)$. Fomin's reversal theorem for a full square growth diagram states that rotating the square by $180^\circ$ and then reading the ordinary empty-boundary diagram with the rotated mark set sends each northeast RSK boundary tableau to its Schützenberger evacuation. Applying this characterization to the east boundary chain of $\Gamma_\pi$, the east boundary tableau $P(\pi)$ becomes the east boundary tableau of the ordinary empty-boundary growth diagram for $\pi^\vee$, and applying the same characterization to the north boundary chain of $\Gamma_\pi$, the north boundary tableau $Q(\pi)$ becomes the north boundary tableau of the ordinary empty-boundary growth diagram for $\pi^\vee$, hence \begin{align*} P(\pi^\vee)=\operatorname{evac}_n(P(\pi)),\qquad Q(\pi^\vee)=\operatorname{evac}_n(Q(\pi)). \end{align*} This proves the stated compatibility between RSK and reverse-complementation. [/step]

[step:Apply the rotation twice to prove evacuation is an involution] Let $T$ be a standard Young tableau with entries $\{1,\dots,n\}$, and let \begin{align*} \varnothing=\lambda_0\subset\lambda_1\subset\cdots\subset\lambda_n \end{align*} be the saturated Young-lattice chain encoding $T$. By the growth-diagram characterization of $\operatorname{evac}_n$ fixed in the theorem statement, $\operatorname{evac}_n(T)$ is obtained by applying the reversible triangular Fomin local rule to the saturated boundary chain encoding $T$ and reading the opposite boundary chain. Applying $\operatorname{evac}_n$ a second time applies the same triangular reversal procedure to that opposite boundary chain. By the uniqueness assumption for the triangular evacuation diagram, the first application constructs a unique triangular labelled diagram whose input boundary is $(\lambda_0,\dots,\lambda_n)$ and whose opposite boundary encodes $\operatorname{evac}_n(T)$. When the opposite boundary is used as the input for the second application, reversibility of the Fomin local rule reconstructs that same triangular labelled diagram in the reverse direction, because each local square determines any one corner from the other three corners together with the mark/no-mark datum. Equivalently, in the square model, the underlying grid rotation is the map \begin{align*} (i,j)\mapsto(n-i,n-j) \end{align*} and this map is an involution. Hence every partition label in the evacuation growth diagram returns to its original position. Therefore the boundary chain encoding $\operatorname{evac}_n(\operatorname{evac}_n(T))$ is again \begin{align*} \varnothing=\lambda_0\subset\lambda_1\subset\cdots\subset\lambda_n. \end{align*} The chain-to-tableau correspondence is injective, because the box containing $k$ is uniquely $\lambda_k\setminus\lambda_{k-1}$. Hence \begin{align*} \operatorname{evac}_n(\operatorname{evac}_n(T))=T. \end{align*} [/step]

[step:Relate the growth-diagram construction to jeu de taquin evacuation] By definition in the formalized statement, $\operatorname{evac}_n$ denotes Schützenberger evacuation in its usual jeu de taquin form, and the same definition includes the equivalent Fomin triangular growth-diagram model as the computational characterization of that map. Thus the boundary-chain identities proved above for the Fomin model are identities for the already-defined map $\operatorname{evac}_n$ on $\operatorname{SYT}_n$. Therefore the RSK reverse-complement identities and the involution identity hold for Schützenberger evacuation, as claimed. [/step]