\begin{proposition}\label{phi-minimizer-zero-distance}\lean{dist_of_min_eq_zero}\leanok  If $X_1,X_2$ is a $\phi$-minimizer, then $d[X_1;X_2] = 0$.
\end{proposition}
\begin{proof}\leanok
  \uses{rho-BSG-triplet-symmetrized,rho-increase-symmetrized,I1-I2-diff,phi-first-estimate,phi-second-estimate}
Consider $T_1:=X_1+X_2,T_2:=X_1+\tilde X_1, T_3:=\tilde X_1 + X_2$, and $S=X_1+X_2+\tilde X_1 + \tilde X_2$. Note that $T_1+T_2+T_3=0$.
First apply \Cref{rho-BSG-triplet-symmetrized} on $(T_1,T_2,T_3)$ when conditioned on $S$ to get
\begin{align}  \label{eq:further-bsg}
d[X_1;X_2] &\leq  \sum_{1 \leq i<j \leq 3} \bbI[T_i:T_j\mid S] + \frac{\eta}{3}   \sum_{1 \leq i<j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -\rho(X_1)-\rho(X_2))\nonumber\\
&= (I_1+2I_2) + \frac{\eta}{3}   \sum_{1 \leq i<j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -\rho(X_1)-\rho(X_2)).
\end{align}
Then apply \Cref{rho-increase-symmetrized} on $(X_1,X_2,\tilde X_1,\tilde X_2)$ and get
$$\sum_{1 \leq i<j \leq 3} (\rho(T_i|T_j,S) + \rho(T_j|T_i,S) -  \rho(X_1)-\rho(X_2))\le (4d[X_1;X_2]+d[X_1;X_2]+d[X_2;X_2])= 6 d[X_1;X_2]+(I_2-I_1)$$
by \Cref{I1-I2-diff}. Plug in the inequality above to (\ref{eq:further-bsg}), we get
$$d[X_1;X_2] \le (I_1+2I_2)+2\eta d[X_1;X_2]+\frac{\eta}{3}(I_2-I_1).$$
By \Cref{phi-second-estimate} we can conclude that
$$d[X_1;X_2] \le 8\eta d[X_1;X_2]-\frac{3-10\eta}{3-3\eta} (2\eta d[X_1;X_2]-I_1).$$
Finally by \Cref{phi-first-estimate} and $\eta<1$ we get that the second term is $\le 0$, and thus $d[X_1;X_2] \le 8\eta d[X_1;X_2]$. By the choice $\eta<1/8$ and the non-negativity of $d$ we have $d[X_1;X_2]=0$.
\end{proof}
theorem dist_of_min_eq_zero (hA : A.Nonempty) (hη' : η < 1/8) : d[X₁ # X₂] = 0 := by
  let ⟨Ω', m', μ, Y₁, Y₂, Y₁', Y₂', hμ, h_indep, hY₁, hY₂, hY₁', hY₂', h_id1, h_id2, h_id1', h_id2'⟩
    := independent_copies4_nondep hX₁ hX₂ hX₁ hX₂ ℙ ℙ ℙ ℙ
  rw [← h_id1.rdist_eq h_id2]
  let _ : MeasureSpace Ω' := ⟨μ⟩
  have : IsProbabilityMeasure (ℙ : Measure Ω') := hμ
  have h'_min : phiMinimizes Y₁ Y₂ η A ℙ := phiMinimizes_of_identDistrib h_min h_id1.symm h_id2.symm
  exact dist_of_min_eq_zero' hη h'_min (h_id1.trans h_id1'.symm) (h_id2.trans h_id2'.symm)
     h_indep hY₁ hY₂ hY₁' hY₂'  hA hη'

open Filter
open scoped Topology

/-- For `η ≤ 1/8`, there exist phi-minimizers `X₁, X₂` at zero Rusza distance. For `η < 1/8`,
all minimizers are fine, by `dist_of_min_eq_zero`. For `η = 1/8`, we use a limit of
minimizers for `η < 1/8`, which exists by compactness. -/