jcost_divergence_eq_zero_iff
plain-language theorem explainer
The theorem establishes that the J-cost divergence between two strictly positive distributions q and p vanishes if and only if the distributions are identical pointwise. Thermodynamic derivations in the recognition framework cite this to confirm uniqueness of the equilibrium that maximizes entropy under fixed average J-cost. The proof splits the biconditional via constructor, extracts vanishing summands from nonnegativity plus the zero condition on Jcost, and reverses by direct substitution.
Claim. Let $D_J(q || p) = sum_ω p(ω) J(q(ω)/p(ω))$ where $J(x) = (x + x^{-1})/2 - 1$ for $x > 0$. Then $D_J(q || p) = 0$ if and only if $q = p$ pointwise, whenever $p(ω) > 0$ and $q(ω) > 0$ for every ω.
background
J-cost is the functional $J(x) = (x + x^{-1})/2 - 1$, nonnegative by the AM-GM inequality with equality solely at unity. The J-cost divergence is the sum $sum p(ω) J(q(ω)/p(ω))$ over the finite index set Ω, measuring discrepancy between positive distributions in the many-body ledger. This module shows Shannon entropy arises as the quadratic approximation to J-cost near equilibrium, with the Gibbs distribution forced by constrained optimization on recognition subsystems.
proof idea
Constructor splits the biconditional. Forward: unfold the sum, prove each summand nonnegative via Jcost_nonneg and the positivity hypotheses, apply Finset.sum_eq_zero_iff_of_nonneg to obtain that every term is zero, then use Jcost_eq_zero_iff on the ratio to recover q(ω) = p(ω). Converse: apply Finset.sum_eq_zero and simplify each term to zero by substitution and Jcost_unit0.
why it matters
Supplies the zero-condition clause inside entropyAncestorCert, which certifies J-cost as the ancestor of entropy by collecting the divergence nonnegativity, uniqueness, and the domination inequality jcost_dominates_squared_log. It closes the step showing the equilibrium distribution is unique under J-cost constraints, confirming that Gibbs weights are theorems of optimization. The result anchors the ancestor hierarchy in which J-cost strictly dominates squared logarithmic terms, consistent with the module's unification of Cost.lean and RecognitionThermodynamics.lean.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.