Thermodynamics Jcost Entropy Ancestor

The thermodynamic bridge

In classical statistical mechanics, the probability that a system occupies a state with energy E is given by the Boltzmann factor, proportional to exp(−E/kT). This exponential form is normally taken as a postulate, justified by its consequences. The Recognition Science module called JCostEntropyAncestor proves that this form is not a postulate but a theorem, derived from counting distinct configurations of a many-body system.

The starting point is a ledger, a discrete record of recognition events, where each event carries a cost. The cost function, denoted J(x), is not arbitrary; it is forced to be J(x) = ½(x + x⁻¹) − 1 by the framework's foundational theorem. The module considers M independent recognition subsystems, each choosing among K possible states, with costs J(r₁), …, J(r_K). The number of microstates realizing a macrodistribution p is the multinomial coefficient Ω(p) = M! / ∏(Mpᵢ)!. By Stirling's approximation, log Ω ≈ M × H(p), where H(p) = −Σ pᵢ log pᵢ is the Shannon entropy.

The key step is constrained optimization. The average cost is fixed, Σ pᵢ J(rᵢ) = E. The most probable macrodistribution is the one that maximizes the entropy H(p) subject to this cost constraint. Solving this with Lagrange multipliers yields the Gibbs measure: p*ᵢ = exp(−J(rᵢ)/T_R) / Z, where T_R is the Lagrange multiplier and Z = Σ exp(−J(rᵢ)/T_R) is the partition function. The module proves this result formally: the theorem entropy_maximizer_is_gibbs states that the Gibbs measure minimizes the free energy, and gibbs_unique proves this minimizer is unique.

The module also establishes the ancestral relationship between J-cost and entropy. A proved inequality, jcost_dominates_squared_log, shows that J(x) ≥ (log x)²/2 for all x > 0. This means the cost function is always at least as large as half the squared logarithm. Since Shannon entropy is built from logarithms, it appears as the second-order approximation of J-cost near equilibrium. The module formalizes this in the structure EntropyAncestorCertificate, which bundles the key theorems: the Gibbs log-form, the dominance inequality, the non-negativity of the J-cost divergence, and the free-energy identity.

In plain language, the module shows that the exponential Boltzmann factor is not a convention but a consequence of counting possibilities. The temperature T_R is not a free parameter but emerges as the Lagrange multiplier enforcing the cost constraint. The framework's cost function is a more fundamental object than entropy, which appears as its shadow. This reverses the usual logical order: instead of assuming entropy and deriving probabilities, the framework derives both from a single, forced cost function.

What this changes is the status of statistical mechanics within the framework. The Gibbs measure, the partition function, and the free energy are not imported from physics but derived from the same cost function that forces the golden ratio and three spatial dimensions. The module provides a bridge from the microscopic ledger to macroscopic thermodynamics, making the exponential law a theorem rather than an axiom.

/-- **BRIDGE THEOREM 2**: The Gibbs distribution is the UNIQUE minimizer
    of free energy. Combined with the counting argument, this means:
    the most probable macrostate IS the Gibbs distribution. -/
theorem gibbs_unique (sys : RecognitionSystem) (X : Ω → ℝ)
    (q : ProbabilityDistribution Ω)
    (h_eq : recognition_free_energy sys q.p X =
            recognition_free_energy sys (gibbs_measure sys X) X) :
    ∀ ω, q.p ω = gibbs_measure sys X ω :=
  gibbs_unique_minimizer sys X q h_eq

/-- **THEOREM (Entropy Functional from Counting)**:
    The free energy F_R(p) = Σ pᵢ J(rᵢ) − T_R × H(p) naturally arises
    from the combined optimization: maximize microstate count (∝ exp(M·H))
    subject to fixed average J-cost (Σ pᵢ J = E).

    The Lagrangian is: L(p) = M·H(p) − β·M·(Σ pᵢ J(rᵢ) − E) − λ·(Σ pᵢ − 1)
    ∂L/∂pᵢ = 0 gives: −M·(log pᵢ + 1) − β·M·J(rᵢ) − λ = 0
    ⟹ log pᵢ = −β·J(rᵢ) − (1 + λ/M)
    ⟹ pᵢ ∝ exp(−β·J(rᵢ))

    This IS the Gibbs distribution with T_R = 1/β. -/
theorem entropy_maximizer_is_gibbs {K : ℕ} [hK : Fact (0 < K)]
    (ledger : ManyBodyLedger K) (sys : RecognitionSystem) :
    let p := gibbs_measure sys (fun i : Fin K => ledger.ratios i)
    ∀ q : ProbabilityDistribution (Fin K),
    recognition_free_energy sys p (fun i => ledger.ratios i) ≤
    recognition_free_energy sys q.p (fun i => ledger.ratios i) := by
  haveI : Nonempty (Fin K) := ⟨⟨0, Fact.out⟩⟩
  intro p q
  exact gibbs_minimizes_free_energy_basic sys (fun i => ledger.ratios i) q

/-- **J-COST DOMINATES SQUARED LOG**: J(x) ≥ (log x)² / 2 for all x > 0.

    This is the Ancestor Inequality in ratio coordinates.
    It means J-cost captures MORE information than (log x)²,
    which is the Fisher information metric. Shannon entropy
    (which uses log linearly) is a weaker, linearized shadow of J-cost. -/
theorem jcost_dominates_squared_log (x : ℝ) (hx : 0 < x) :
    Jcost x ≥ (log x) ^ 2 / 2 := by
  have h := cosh_sub_one_ge_sq_div_two (log x)
  have hJ : Jlog (log x) = Jcost x := by
    simp [Jlog, exp_log hx]
  rw [← hJ, Jlog_as_cosh]
  exact h

/-- The Gibbs measure satisfies log p(ω) = −J(X(ω))/T_R − log Z.
    This is the "Gibbs log-form": log-probability is affine in J-cost. -/
theorem gibbs_log_form (sys : RecognitionSystem) (X : Ω → ℝ) (ω : Ω) :
    log (gibbs_measure sys X ω) = -Jcost (X ω) / sys.TR - log (partition_function sys X) := by
  unfold gibbs_measure gibbs_weight
  have hZ := partition_function_pos sys X
  rw [log_div (exp_pos _).ne' hZ.ne', log_exp]

What this page does not claim

The module does not prove the Stirling approximation itself. The module does not claim that all physical systems are ledgers. The module does not derive the numerical value of the temperature T_R.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Thermodynamics/JCostEntropyAncestor.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: