kl_divergence_zero_iff_eq
plain-language theorem explainer
The declaration shows that the Kullback-Leibler divergence between two normalized distributions on a finite set vanishes if and only if the distributions coincide pointwise. Researchers deriving the Gibbs state from cost-constrained maximum entropy would cite it to obtain uniqueness. The proof defines a non-negative excess function, uses the sum-to-zero property to force each term to vanish, and handles the q=0 boundary via order antisymmetry and the strict convexity inequality log y < y-1.
Claim. Let $Ω$ be a finite set. Let $q,p:Ω→ℝ$ satisfy $q≥0$, $p>0$, $∑_ω q(ω)=1$ and $∑_ω p(ω)=1$. Then the Kullback-Leibler divergence $D_{KL}(q∥p)=0$ if and only if $q(ω)=p(ω)$ for every $ω∈Ω$.
background
The module derives the Gibbs distribution as the equilibrium that maximizes entropy subject to a recognition cost constraint. The KL divergence supplies the information-theoretic penalty that appears inside the free-energy functional. Upstream arithmetic results from ArithmeticFromLogic provide the non-strict order (le) and its antisymmetry (le_antisymm) together with the multiplication rule mul_zero, all used to control the boundary where q vanishes at isolated points. LedgerFactorization calibrates the underlying J-cost that induces the free-energy expression.
proof idea
The tactic proof opens with constructor. The forward direction defines an excess term equal to the KL integrand minus (q-p) when both are positive and zero otherwise. Non-negativity of excess follows from log_le_sub_one_of_pos after rewriting the ratio. The sum of excesses collapses to zero because the KL sum is assumed zero and ∑(q-p)=0 by normalization. The sum-equals-zero lemma for non-negative functions then yields pointwise vanishing. Case analysis on q(ω)>0 produces the equality log(q/p)=1-p/q; the converse assumption q≠p yields p/q≠1 and contradicts the strict inequality log y < y-1 via Real.add_one_lt_exp. The reverse direction substitutes q=p directly and observes that every summand collapses to zero.
why it matters
The result is invoked inside gibbs_unique_minimizer to convert equality of free energies into pointwise equality of distributions. It thereby supplies the uniqueness half of the maximum-entropy derivation in the Recognition Science thermodynamics module. The characterization underwrites the emergence of the Gibbs measure from the J-cost functional, consistent with the self-similar fixed point phi and the discrete ladder that discretizes thermodynamic states.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.