mf_critical_temperature
plain-language theorem explainer
The mean-field critical temperature TRc,MF is defined as 3 times the square of the natural logarithm of the golden ratio phi, yielding approximately 0.694 for d=3 and z=6. Researchers analyzing phase transitions in the GCIC model cite this constant when working with mean-field approximations. The declaration is a direct noncomputable definition that evaluates the expression using the phi constant from the CPM bundle.
Claim. $T_{c, MF} = 3 (ln φ)^2$ where φ is the golden ratio.
background
The GCIC Phase Thermodynamics module formalizes constants from the GCIC Response paper 'Two Upgrades for the GCIC Paper' (Feb 2026), focusing on stiffness, barrier, and phase structure for the model. The definition draws phi from the Constants structure in LawOfExistence, an abstract bundle that includes Knet, Cproj, Ceng, Cdisp and related nonnegativity conditions. This supplies the mean-field critical temperature for spatial dimension d=3 and coordination number z=6 in the Recognition Science setting.
proof idea
The declaration is a direct definition that computes three times the square of Real.log applied to Constants.phi. No lemmas or tactics are invoked beyond the definition itself.
why it matters
This constant is referenced by gcic_thermodynamics_cert, mf_critical_temperature_bounds, mf_critical_temperature_pos, and mf_temp_eq_six_kappa. It supplies the mean-field critical temperature value from the GCIC paper and connects to the forcing chain landmarks T7 (eight-tick octave) and T8 (D=3 spatial dimensions). The definition supports the uniform convexity analysis of the phase potential via the downstream certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.