IndisputableMonolith.Papers.GCIC.Thermodynamics
This module develops thermodynamic relations for the GCIC model inside Recognition Science. It supplies the inequality log(phi) > 0.48 together with positivity and bound statements for stiffness, phase barriers, and mean-field critical temperatures. The results rest on interval arithmetic for logarithms and on the cost landscape imported from DiscretenessForcing. The module is organized as a sequence of paired definition-plus-lemma blocks rather than a single central theorem.
claim$\log\phi > 0.48$, gcic stiffness function, phase barrier function, and mean-field critical temperature, each equipped with positivity and explicit numerical bounds derived from the J-cost minimum.
background
The module imports Constants (where $\tau_0 = 1$ tick), Cost, DiscretenessForcing, and Numerics.Interval.Log. DiscretenessForcing states that J(x) = ½(x + x⁻¹) - 1 attains its unique minimum at x = 1 and, in logarithmic coordinates, becomes the convex function cosh(t) - 1 centered at t = 0. Numerics.Interval.Log supplies rigorous interval bounds on the natural logarithm via Taylor series with explicit error control. These ingredients are applied to GCIC thermodynamic quantities.
proof idea
The module consists of a chain of lemmas that first record the inherited numerical bound log(phi) > 0.48, then define each thermodynamic object and immediately prove its positivity and explicit bounds. Each block follows the pattern definition, _pos theorem, _bounds theorem, relying on the interval log machinery and the convexity properties of the J-cost.
why it matters in Recognition Science
The module supplies the thermodynamic layer that connects the cost-forced discreteness of DiscretenessForcing to phase-transition phenomena in the GCIC setting. It prepares the ground for any later analysis of critical behavior or stiffness-driven dynamics within the Recognition Science papers, although the current dependency graph lists no direct downstream users.
scope and limits
- Does not derive a full partition function or statistical mechanics from the J-cost.
- Does not treat fluctuations beyond the mean-field approximation.
- Does not incorporate spatial dependence or explicit D = 3 geometry.
- Does not address time-dependent or non-equilibrium thermodynamics.
depends on (4)
declarations in this module (16)
-
lemma
log_phi_gt_048 -
lemma
log_phi_lt_0483 -
def
gcic_stiffness -
theorem
gcic_stiffness_pos -
theorem
gcic_stiffness_bounds -
def
phase_barrier -
theorem
phase_barrier_pos -
theorem
phase_barrier_lower -
theorem
phase_barrier_upper -
def
mf_critical_temperature -
theorem
mf_critical_temperature_pos -
theorem
mf_critical_temperature_bounds -
theorem
mf_temp_eq_six_kappa -
theorem
noncompact_uniform_convexity -
theorem
jlog_above_half_square -
theorem
gcic_thermodynamics_cert