Papers Gcic Thermodynamics
GCIC Phase Thermodynamics is a Lean module that formalizes the key constants of a phase structure derived from the golden ratio, including a stiffness, a barrier, and a critical temperature.
GCIC Phase Thermodynamics
GCIC Phase Thermodynamics is a formal module in the Recognition Science library that fixes the numerical constants of a phase transition. The module takes the golden ratio phi, the unique self-similar scaling forced by the recognition cost function, and derives from it three quantities: a stiffness constant, a phase barrier, and a mean-field critical temperature. These are not fitted numbers; they are definitions built on the logarithm of phi, and the module proves their positivity and their numerical bounds.
The stiffness constant is defined as κ = (ln φ)²/2, approximately 0.116. The module proves it is positive and lies strictly between 0.1152 and 0.1167. The phase barrier is defined as J̃(1/2) = cosh(ln φ / 2) − 1, approximately 0.029, and is established to be positive and bounded between 0.0287 and 0.032. The mean-field critical temperature is defined as TRc,MF = 3(ln φ)², approximately 0.694, and is established to lie between 0.691 and 0.701. A further theorem shows this temperature is exactly six times the stiffness constant.
The module also establishes a structural property of the phase potential. It proves that the second derivative of the potential is cosh(t), which is always at least 1, giving uniform convexity. From this it derives the quadratic lower bound cosh(t) − 1 ≥ t²/2. A summary certificate bundles the positivity of all three constants with the uniform convexity statement into a single theorem.
In plain language, the module pins down the numbers that describe how a recognition system resists changing its phase, how high the barrier is to switching, and at what temperature the mean-field approximation predicts the transition happens. All of these numbers are forced by the single constant phi, which is itself forced by the recognition cost function. The module is a formal record that these bounds and identities are established in Lean, not merely asserted.
THEOREM gcic_stiffness · gcic_stiffness_pos · gcic_stiffness_bounds · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
THEOREM phase_barrier · phase_barrier_pos · phase_barrier_lower · phase_barrier_upper · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
THEOREM mf_critical_temperature · mf_critical_temperature_pos · mf_critical_temperature_bounds · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
THEOREM mf_temp_eq_six_kappa · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
THEOREM noncompact_uniform_convexity · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
What this page does not claim
This module does not prove that any actual physical system undergoes a phase transition at this temperature. This module does not derive the values from first principles; it defines them in terms of the golden ratio and proves their properties. This module does not claim the mean-field critical temperature is the exact critical temperature of any real material.
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/Papers/GCIC/Thermodynamics.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:
- How does the phase barrier relate to the eight-tick recognition cycle?
- What physical system is the mean-field critical temperature describing?
- What is the empirical status of the predicted critical temperature?
- How does the uniform convexity of the phase potential connect to the uniqueness theorem for the cost function?
MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND
- THEOREMThe stiffness constant is defined as κ = (ln φ)²/2, approximately 0.116, and is established to be positive and lie strictly between 0.1152 and 0.1167. gcic_stiffness · gcic_stiffness_pos · gcic_stiffness_bounds · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
- THEOREMThe phase barrier is defined as J̃(1/2) = cosh(ln φ / 2) − 1, approximately 0.029, and is established to be positive and bounded between 0.0287 and 0.032. phase_barrier · phase_barrier_pos · phase_barrier_lower · phase_barrier_upper · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
- THEOREMThe mean-field critical temperature is defined as T<sub>R</sub><sup>c,MF</sup> = 3(ln φ)², approximately 0.694, and is established to lie between 0.691 and 0.701. mf_critical_temperature · mf_critical_temperature_pos · mf_critical_temperature_bounds · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
- THEOREMA further theorem shows this temperature is exactly six times the stiffness constant. mf_temp_eq_six_kappa · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean
- THEOREMThe module proves that the second derivative of the potential is cosh(t), which is always at least 1, giving uniform convexity. noncompact_uniform_convexity · IndisputableMonolith/Papers/GCIC/Thermodynamics.lean