gcic_thermodynamics_cert
plain-language theorem explainer
The certificate asserts positivity of the GCIC stiffness constant, phase barrier, and mean-field critical temperature together with uniform convexity of cosh. Researchers citing the GCIC Response paper on phase structure would reference this to confirm the thermodynamic parameters are strictly positive before proceeding to free-energy calculations. The proof is a one-line term that packages the four component lemmas.
Claim. Let $k = (ln phi)^2 / 2$, $Delta = cosh((ln phi)/2) - 1$, and $T_{c, MF} = 3 (ln phi)^2$. Then $k > 0$, $Delta > 0$, $T_{c, MF} > 0$, and $cosh t >= 1$ for all real $t$.
background
The module formalizes constants from the GCIC Response paper. GCIC stiffness is defined as $k = (ln phi)^2 / 2$ with phi the golden-ratio fixed point. Phase barrier is the value of the J-cost at half-argument: $Delta = cosh((ln phi)/2) - 1$. Mean-field critical temperature is $T_{c, MF} = 3 (ln phi)^2$ for spatial dimension 3. Noncompact uniform convexity states that the second derivative of the phase potential satisfies $V''(t) = cosh t >= 1$.
proof idea
The term proof directly supplies the four component results: gcic_stiffness_pos, phase_barrier_pos, mf_critical_temperature_pos, and noncompact_uniform_convexity. No further reduction or tactic steps are required.
why it matters
This declaration closes the local thermodynamic certificate for the GCIC phase diagram, confirming that the stiffness, barrier height, and critical temperature are positive before any free-energy or partition-function analysis. It sits downstream of the J-uniqueness and phi-ladder constructions in the forcing chain and supplies the numerical anchors used in the GCIC Response paper. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.