entropyAncestorCert
plain-language theorem explainer
The declaration constructs a certificate structure asserting that J-cost divergence is at least as strong as KL divergence, that the Gibbs measure takes the explicit log-form affine in J-cost, and that the ancestor inequality J(x) >= (log x)^2/2 holds. Researchers deriving thermodynamics from recognition cost functionals cite it to invoke the full bridge at once. The construction is a direct structure instantiation that composes six sibling theorems for the required fields.
Claim. The certificate asserts: for any recognition system and cost function X, log of the Gibbs measure equals -J(X(ω))/T_R - log Z; J(x) >= (log x)^2/2 for all x > 0; the J-cost divergence between positive distributions q and p is nonnegative and equals zero if and only if q = p; the free-energy identity F = <E> - TS holds; and the Gibbs distribution is the unique minimizer of free energy.
background
The module establishes J-cost as the ancestor of Shannon entropy by showing that the Gibbs weights exp(-J/T_R) arise as the unique solution to maximizing entropy subject to fixed average J-cost on a many-body ledger. J-cost is defined as J(x) = (x + x^{-1})/2 - 1, which equals cosh(log x) - 1. The ancestor inequality J(x) >= (log x)^2/2 is the key domination result, implying that squared-log information (Fisher metric) is a quadratic shadow of the full J-cost functional. Entropy emerges only after linearization around the fixed point x = 1. The local setting is the constrained optimization on recognition systems whose microstate counting yields the multinomial coefficient whose Stirling approximation produces Shannon entropy.
proof idea
One-line wrapper that applies the structure constructor to six sibling results: the Gibbs log-form theorem supplies the explicit log-probability expression; the J-cost dominates squared log theorem supplies the ancestor inequality; the nonnegativity and zero-iff theorems supply the divergence properties; the free-energy identity and Gibbs uniqueness theorems complete the certificate fields.
why it matters
It realizes Bridge Theorem 4 in the module, closing the backward direction from cost to entropy and free energy. The certificate feeds the claim that entropy is a linearization of J-cost rather than a primitive, consistent with the Recognition Composition Law and the T5 J-uniqueness fixed point. No downstream uses are recorded yet; the structure is intended as a reusable interface for later derivations of the Boltzmann distribution and variational dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.