jcost_divergence
plain-language theorem explainer
The J-cost divergence between distributions q and p is the sum over states of p(ω) times J-cost of the ratio q(ω)/p(ω) when both are positive, and zero otherwise. Researchers deriving thermodynamics from recognition costs cite it as the divergence native to the J-cost functional. The definition is introduced directly as a conditional sum with no lemmas applied.
Claim. For probability distributions q and p on a finite set Ω, the J-cost divergence is defined by D_J(q || p) = ∑_ω p(ω) J(q(ω)/p(ω)) where the sum runs only over ω with p(ω) > 0 and q(ω) > 0, and J(x) = ½(x + x^{-1}) - 1.
background
This definition sits inside the module that derives J-cost as the ancestor of Shannon entropy. The J-cost functional J(x) = ½(x + x^{-1}) - 1 satisfies the Recognition Composition Law and supplies the energy term in constrained optimization over many-body ledgers. The module shows that the Gibbs measure exp(-J/T_R)/Z arises as the unique maximizer of entropy subject to fixed average J-cost, with T_R = 1/β the Lagrange multiplier.
proof idea
This is a direct definition that unfolds to a finite sum over the state space, inserting the term p(ω) * Jcost(q(ω)/p(ω)) only when both probabilities are strictly positive and zero otherwise.
why it matters
The definition supplies the divergence used in the EntropyAncestorCertificate structure and in the theorems jcost_divergence_nonneg, jcost_divergence_eq_zero_iff, and jcost_div_ge_half_chi_squared. It completes the bridge from the J-cost functional to the thermodynamic structures, showing that Shannon entropy is the quadratic linearization of J-cost via the ancestor inequality J(x) ≥ (log x)^2 / 2. It touches the T5 J-uniqueness step and the emergence of thermodynamics from recognition constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.