\begin{theorem}[$\tau$-decrement]\label{de-prop}
  \lean{tau_strictly_decreases}\leanok
  Let $X_1, X_2$ be tau-minimizers.  Then $d[X_1;X_2] = 0$.
\end{theorem}
\begin{proof}
  \uses{construct-good, key-ident, uvw-s, total-dist, first-estimate, eta-def}\leanok
  Set $k := d[X_1;X_2]$.  Applying \Cref{construct-good} with any random variables $(T_1,T_2,T_3)$ such that $T_1+T_2+T_3=0$ holds identically, we deduce that
\[
  k \leq \delta + \frac{\eta}{3} \biggl( \delta + \sum_{i=1}^2 \sum_{j = 1}^3 (d[X^0_1;T_j] - d[X^0_i;X_i]) \biggr).
\]
Note that $\delta$ is still defined by~\eqref{delta-t1t2t3-def} and thus depends on $T_1,T_2,T_3$.
In particular we may apply this for
\[
  T_1 = (U | S = s),\qquad T_2 = (V | S = s), \qquad T_3 = (W | S = s)
\]
for $s$ in the range of $S$ (which is a valid choice by \Cref{key-ident}) and then average over $s$ with weights $p_S(s)$, to obtain
\[k \leq \tilde \delta + \frac{\eta}{3} \biggl( \tilde \delta + \sum_{i=1}^2 \sum_{A\in\{U,V,W\}} \bigl(  d[X^0_i;A|S] - d[X^0_i;X_i]\bigr) \biggr),\]
where
\[
  \tilde \delta :=  \bbI[U : V | S] + \bbI[V : W | S] + \bbI[W : U | S].
\]
Putting this together with \Cref{uvw-s} and \Cref{total-dist}, we conclude that
\begin{align*}
  k &\leq \Bigl(1+\frac{\eta}{3}\Bigr)\Bigl(6\eta k-\frac{1-5\eta}{1-\eta}(2\eta k-I_1)\Bigr)+\frac{\eta}{3}\Bigl((6-3\eta)k+3(2\eta k-I_1)\Bigr)\\
  &= (8\eta + \eta^2) k - \biggl( \frac{1 - 5 \eta}{1-\eta}\Bigl(1 + \frac{\eta}{3}\Bigr) -  \eta \biggr)(2 \eta k - I_1)\\
  &\leq (8 \eta + \eta^2) k
 \end{align*}
since the quantity $2 \eta k - I_1$ is non-negative (by \Cref{first-estimate}), and its coefficient in the above expression is non-positive provided that $\eta(2\eta + 17) \le 3$, which is certainly the case with \Cref{eta-def}.
Moreover, from \Cref{eta-def} we have $8 \eta + \eta^2 < 1$. It follows that $k=0$, as desired.
\end{proof}
theorem tau_strictly_decreases (h_min : tau_minimizes p X₁ X₂) (hpη : p.η = 1/9) :
    d[X₁ # X₂] = 0 := by
  let ⟨A, mA, μ, 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 A := ⟨μ⟩
  have : IsProbabilityMeasure (ℙ : Measure A) := hμ
  rw [← h_id1.tau_minimizes p h_id2] at h_min
  apply tau_strictly_decreases_aux p Y₁ Y₂ Y₁' Y₂' hY₁ hY₂ hY₁' hY₂' (h_id1.trans h_id1'.symm)
    (h_id2.trans h_id2'.symm) h_indep h_min hpη

/-- `entropic_PFR_conjecture`: For two $G$-valued random variables $X^0_1, X^0_2$, there is some
    subgroup $H \leq G$ such that $d[X^0_1;U_H] + d[X^0_2;U_H] \le 11 d[X^0_1;X^0_2]$. -/