EntropyAncestorCertificate
plain-language theorem explainer
EntropyAncestorCertificate packages the properties establishing that J-cost divergence dominates KL divergence while the Gibbs distribution emerges uniquely from free-energy minimization on recognition systems. A researcher deriving the second law from a constrained cost functional would cite this structure to close the thermodynamic bridge. It is assembled as a record whose fields reference prior lemmas for the ancestor inequality, divergence non-negativity, and free-energy identities.
Claim. A structure asserting the following for a recognition system with temperature parameter $T_R$ and observable $X$ on finite state space $Ω$: (i) the logarithm of the Gibbs measure satisfies $log(gibbs(ω)) = -J(X(ω))/T_R - log Z$ where $Z$ is the partition function; (ii) $J(x) ≥ (log x)^2/2$ for all $x > 0$; (iii) the J-cost divergence $D_J(q,p) ≥ 0$ for positive distributions $q,p$; (iv) $D_J(q,p) = 0$ if and only if $q = p$; (v) the recognition free energy of the Gibbs measure equals $-T_R log Z$; (vi) the Gibbs measure is the unique minimizer of recognition free energy; (vii) the free-energy gap equals $T_R$ times the KL divergence.
background
In this module J-cost is the functional $J(x) = ½(x + x^{-1}) - 1$ imported from the Cost layer. A RecognitionSystem is a finite state space equipped with the recognition temperature $T_R$. The J-cost divergence is defined by $D_J(q || p) = ∑ p(ω) J(q(ω)/p(ω))$. Upstream results supply the Gibbs measure $p(ω) = exp(-J(X(ω))/T_R)/Z$, the partition function $Z = ∑ exp(-J/T_R)$, the KL divergence $D_{KL}(q || p) = ∑ q log(q/p)$, and the recognition free energy $F_R = -T_R log Z$ for the Gibbs state.
proof idea
The declaration is a structure definition. Each field is witnessed directly by an earlier lemma in the same module: gibbs_log by gibbs_log_form, ancestor_ineq by jcost_dominates_squared_log, jcost_div_nonneg and jcost_div_zero_iff by the corresponding divergence lemmas, free_energy_natural by free_energy_identity, gibbs_uniqueness by the uniqueness lemma, and gap_is_kl by the gap identity. No further tactics are applied.
why it matters
This structure completes the backward derivation from the Recognition Composition Law through J-cost to the emergence of Shannon entropy and the second law. It is instantiated by entropyAncestorCert, which wires the specific lemmas into a single certificate. The result shows entropy is the quadratic shadow of J-cost via the ancestor inequality $J(x) ≥ (log x)^2/2$, consistent with the module's hierarchy. It touches the open question of how the derived $T_R$ connects to the fundamental constants obtained from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.