RECOGNITION ENCYCLOPEDIA COMPILED 2026-08-06 · PUBLIC EDITION · SOURCES: 1 LEAN MODULE

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND