module module high

`IndisputableMonolith.Thermodynamics.JCostEntropyAncestor`

The JCostEntropyAncestor module establishes the Gibbs log-form relating log-probability to J-cost at finite recognition temperature in Recognition Science. Researchers deriving statistical ensembles from cost minimization would cite it when extending T=0 minimization to finite TR. The module assembles the affine relation from imported cost and max-ent results without new proofs.

claim$\log p(\omega) = -J(X(\omega))/T_R - \log Z$, where $J$ denotes the J-cost, $T_R$ the recognition temperature, and $Z$ the partition function.

background

Recognition Science extends the T=0 cost minimization (J=0) to finite Recognition Temperature TR, which parameterizes the strictness of J-minimization. MaxEntFromCost proves that the Gibbs distribution emerges from the principle of maximum entropy subject to a cost constraint. The module imports Cost for the J-cost definition and RecognitionThermodynamics for the TR parameter, focusing on the ancestor relation that log-probability is affine in J-cost.

proof idea

This is a definition module, no proofs. It contains the Gibbs log-form statement together with sibling lemmas on divergence non-negativity and uniqueness that follow directly from the imported max-ent and recognition-thermodynamics results.

why it matters in Recognition Science

The module supplies the Gibbs log-form that underpins the statistical mechanics extension from T=0 to finite TR. It feeds downstream entropy and thermodynamic potential calculations in the Recognition framework and directly implements the affine cost-probability link required by the maximum-entropy derivation.

scope and limits

Does not compute explicit values for the partition function Z.
Does not derive numerical bounds on the recognition temperature TR.
Does not address quantum or field-theoretic extensions of the measure.
Does not prove uniqueness of the Gibbs form outside the max-ent setting.

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