module module high

`IndisputableMonolith.Thermodynamics.JCostEntropyAncestor`

This module establishes the Gibbs log-form relating J-cost to probability in Recognition Science thermodynamics. It shows that the maximum-entropy distribution under a J-cost constraint takes the explicit affine form log p(ω) = −J(X(ω))/T_R − log Z. Researchers deriving thermodynamic relations from cost minimization cite it as the bridge between zero-temperature recognition and finite-temperature statistics. The module imports the general max-ent result from MaxEntFromCost and specializes it to the J-cost functional defined in the Cost module.

claimThe equilibrium distribution satisfies $log p(ω) = -J(X(ω))/T_R - log Z$, where $J$ is the J-cost, $T_R$ the recognition temperature, and $Z$ the partition function.

background

Recognition Science extends zero-temperature J-minimization to finite recognition temperature T_R, which controls the strictness of the cost constraint. The upstream MaxEntFromCost module proves that the Gibbs distribution emerges from maximum entropy subject to a cost constraint. RecognitionThermodynamics supplies the statistical-mechanics setting in which J-cost replaces the usual energy function. The present module specializes that general result to the J-cost functional, yielding the explicit log-probability form quoted in the module doc-comment.

proof idea

This is a definition module, no proofs. It imports the max-ent theorem from MaxEntFromCost, the J-cost definition from Cost, and the temperature parameterization from RecognitionThermodynamics, then records the resulting Gibbs log-form as the ancestor relation between J-cost and entropy.

why it matters in Recognition Science

The module supplies the explicit link between J-cost minimization and thermodynamic entropy that later results on potentials and phase structure require. It fills the step from the T=0 forcing chain to finite-temperature statistics in the Recognition framework. No downstream uses are recorded yet, but the Gibbs log-form is the direct ancestor of all subsequent thermodynamic identities built on J-cost.

scope and limits

Does not compute the explicit partition function Z for any concrete J.
Does not address non-equilibrium or time-dependent processes.
Does not incorporate quantum statistics or field-theoretic extensions.
Does not derive fluctuation-dissipation relations or response functions.

depends on (3)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Thermodynamics.MaxEntFromCost module_import
IndisputableMonolith.Thermodynamics.RecognitionThermodynamics module_import

declarations in this module (22)

theorem gibbs_log_form L71
theorem gibbs_form_is_unique L80
theorem lagrange_forces_gibbs L94
def jcost_divergence L137
theorem jcost_divergence_nonneg L140
theorem jcost_divergence_eq_zero_iff L149
lemma exp_sum_minus_two_eq_sq L185
theorem cosh_sub_one_ge_sq_div_two L200
theorem jcost_dominates_squared_log L226
theorem ancestor_inequality_tight_at_one L236
structure ManyBodyLedger L259
structure Macrostate L266
def avg_jcost L279
class StirlingApproximation L286
theorem entropy_maximizer_is_gibbs L305
theorem temperature_from_constraint L322
theorem free_energy_is_natural L343
theorem gibbs_unique L351
theorem free_energy_gap_is_kl L361
theorem jcost_div_ge_half_chi_squared L374
structure EntropyAncestorCertificate L401
def entropyAncestorCert L426