mf_critical_temperature_pos
plain-language theorem explainer
Mean-field critical temperature TRc,MF equals 3 (ln φ)^2 and is strictly positive. Researchers formalizing phase transitions in the GCIC framework cite this positivity to confirm thermodynamic consistency for d=3 lattices. The term-mode proof unfolds the definition and applies mul_pos to the constant 3 together with the square of a positive logarithm.
Claim. $0 < 3 (ln φ)^2$ where $φ$ denotes the golden ratio and the left-hand side is the mean-field critical temperature $T_{c, MF}$ for coordination number 6 in three dimensions.
background
The GCIC Phase Thermodynamics module formalizes constants from the GCIC Response paper 'Two Upgrades for the GCIC Paper' (Feb 2026), with emphasis on stiffness, barrier height, and phase structure. The mean-field critical temperature is introduced via the definition mf_critical_temperature := 3 * (Real.log Constants.phi)^2, which evaluates numerically near 0.694 for d=3 and z=6. This construction rests on the CPM constants bundle and on the elementary inequality 1 < phi proved in Constants.one_lt_phi by comparing square roots: Real.sqrt 1 < Real.sqrt 5 implies 2 < 1 + Real.sqrt 5.
proof idea
The term proof first unfolds mf_critical_temperature to obtain the product 3 * (log phi)^2. It then invokes mul_pos, supplying a norm_num witness that 3 > 0, and finishes with pow_pos applied to Real.log_pos of the fact 1 < phi supplied by Constants.one_lt_phi.
why it matters
The result is consumed directly by gcic_thermodynamics_cert, which packages positivity of stiffness, phase barrier, and this critical temperature into a single certificate theorem. It supplies the elementary positivity step required by the mean-field temperature bound in the GCIC paper upgrades and aligns with the Recognition Science forcing chain at T8 (D=3) and the eight-tick octave. No open scaffolding remains; the declaration closes a basic sign check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.