Maximum independent edge set conjecture for 3-token graphs of paths

Let $P_n$ be the path graph on $n$ vertices, and let $\Gamma_3(P_n)$ denote its $3$-token graph. Write $\alpha'(G)$ for the maximum size of an independent edge set in a graph $G$. For any $n\geq 3$, the $3$-token graph $\Gamma_3(P_n)$ satisfies

Maximum independent edge set conjecture.

$$\alpha'(\Gamma_3(P_n)) = \begin{cases} \displaystyle \sum_{k=1}^{\frac{n}{2}-1} \left(\sum_{i=1}^{2k-1} i \right)+ \sum_{i=1}^{\frac{n}{2}-1} i, & \text{if } n \text{ is even},\\[6pt] \displaystyle \sum_{k=1}^{\frac{n-1}{2}-1} \left(\sum_{i=1}^{2k} i \right)+ \sum_{i=1}^{\frac{n-1}{2}-1} i, & \text{if } n \text{ is odd}, \end{cases}$$

and equivalently

$$\alpha'(\Gamma_3(P_n)) = \begin{cases} \displaystyle \frac{n^3-3n^2+2n}{12}, & \text{if } n \text{ is even},\\[6pt] \displaystyle \frac{n^3-3n^2-n+3}{12}, & \text{if } n \text{ is odd}. \end{cases}$$

The conjecture asserts that the displayed independent edge sets are maximum. The proposed formulas are based on explicit constructions for even and odd $n$; determining whether these constructions are largest remains an open problem for the $3$-token graphs of path graphs.