jcost_div_ge_half_chi_squared
plain-language theorem explainer
The J-cost divergence between positive probability distributions q and p satisfies a lower bound given by half the p-weighted sum of squared log-ratios. Thermodynamic derivations that start from recognition costs cite this result to show J-cost supplies a strictly stronger inequality than the corresponding Kullback-Leibler form. The proof unfolds the divergence sum, reduces via the finite-sum comparison lemma, and applies the pointwise ancestor bound J(r) ≥ (log r)^2/2 term by term.
Claim. Let $p,q$ be positive real-valued functions on a finite set with $p$ normalized to sum to one. The J-cost divergence $D_J(q||p)$ then obeys $D_J(q||p) ≥ (1/2) ∑ p(ω) [log(q(ω)/p(ω))]^2$.
background
J-cost is the functional J(r) = (r + r^{-1})/2 - 1 arising from the multiplicative recognizer comparator. The J-cost divergence is the expectation D_J(q||p) = ∑ p(ω) J(q(ω)/p(ω)). The module derives Gibbs weights and Shannon entropy as consequences of constrained optimization on many-body ledgers whose microstate count is given by multinomial coefficients; Stirling's approximation then yields entropy as the log-count. Upstream, entropy is defined as total defect of a configuration, and recognition-event cost is identified with J-cost.
proof idea
The tactic proof unfolds the divergence definition, rewrites the target inequality with ge_iff_le and Finset.mul_sum, then invokes Finset.sum_le_sum. For each summand it obtains the positive ratio, applies the ancestor inequality J(r) ≥ (log r)^2/2, and closes the comparison by mul_le_mul_of_nonneg_left together with a ring identity.
why it matters
This is Bridge Theorem 4 inside the ancestor certificate that packages the full chain from the Recognition Composition Law through J-cost, many-body counting, Lagrange optimization, and the second law. It establishes that J-cost dominates the quadratic information measure, so Shannon entropy appears only as the second-order linearization. The result sits between the uniqueness of J (T5) and the emergence of Gibbs structure from ledger constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.