mf_critical_temperature_bounds
plain-language theorem explainer
The mean-field critical temperature TRc,MF in the GCIC thermodynamics model satisfies the strict numerical bounds 0.691 < TRc,MF < 0.701. Researchers calibrating phase transitions and stiffness parameters in recognition-based models would cite this interval when fixing the temperature scale against the phi ladder. The proof unfolds the temperature definition, imports the log-phi interval lemmas, and closes the bounds via nlinarith on squared deviations.
Claim. $0.691 < T_{c, MF} < 0.701$, where $T_{c, MF}$ is the mean-field critical temperature obtained from the GCIC stiffness and phase-barrier expressions.
background
The module formalizes key constants from the GCIC Response paper (Feb 2026) on phase thermodynamics, including stiffness, barrier height, and mean-field critical temperature. Upstream, the Constants structure bundles Knet, Cproj, Ceng, Cdisp with the nonnegativity axiom Knet_nonneg. The log-phi bounds log phi > 0.48 and log phi < 0.483 are established in the Numerics.Interval modules by monotonicity of exp and Taylor bounds on exp(0.48) and exp(0.483), using the golden-ratio bounds 1.61803395 < phi < 1.6180340.
proof idea
The term proof unfolds mf_critical_temperature, obtains the lower bound log phi > 0.48 and upper bound log phi < 0.483 from the respective interval lemmas, then applies nlinarith to the three squared terms (log phi - 0.48)^2, (log phi - 0.483)^2, and (log phi)^2 to obtain the target interval by linear arithmetic.
why it matters
The result supplies a calibrated numerical window for the mean-field critical temperature that anchors the GCIC phase-structure analysis. It directly supports the stiffness and barrier lemmas in the same module and closes a concrete numerical claim from the February 2026 response paper. Within Recognition Science it fixes the temperature scale against the phi fixed point and the eight-tick octave; the absence of downstream uses indicates it functions as a calibration leaf for further thermodynamic derivations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.