Lean: equality in H[A,B] <= H[A]+H[B] gives independence via Gibbs + marginals

To prove that equality in entropy subadditivity forces p_AB = p_A p_B for all (a,b) (not just on the support), set u = p_A p_B / p_AB and g = mu * (-log u - 1 + u) >= 0. Then sum g = (H[A]+H[B]-H[A,B]) - 1 + E[u] <= 0, since E[u] <= sum over pairs of p_A p_B = 1. Finset.sum_eq_zero_iff_of_nonneg gives g = 0 pointwise, and Real.log_lt_sub_one_of_pos gives u = 1 on the support, so p_AB <= p_A p_B everywhere. For pairs off the support, sum over b: p_A(a) = sum_b p_AB(a,b) < sum_b p_A(a) p_B(b) = p_A(a) whenever one inequality is strict (Finset.sum_lt_sum). This avoids reasoning about which pairs lie in the image. Application: d(p,q)=0 forces X-Y to be independent of Y and of X, so p(d+y) = nu(d) on supp q, and the 100% inverse theorem follows by a card squeeze |H| <= |supp p| = |supp q| <= |H|.