gcic_stiffness
plain-language theorem explainer
The GCIC stiffness constant is defined as κ = (ln φ)^2 / 2 ≈ 0.116, where φ is the golden ratio supplied by the Recognition constants bundle. Researchers modeling mean-field critical temperatures and phase barriers in the GCIC framework cite this definition when establishing positivity and interval bounds. The declaration is a direct noncomputable definition with no lemmas or tactics.
Claim. Let κ denote the GCIC stiffness constant. Then κ = (ln φ)^2 / 2, where φ is the golden ratio from the Recognition Science constants bundle.
background
The GCIC Phase Thermodynamics module formalizes key constants from the February 2026 GCIC Response paper on phase structure. Stiffness κ enters mean-field temperature relations and uniform-convexity certificates for the phase potential. The upstream Constants structure from LawOfExistence supplies φ together with Knet, Cproj, Ceng, and Cdisp as an abstract bundle of CPM parameters.
proof idea
The definition is a direct algebraic expression. It squares the natural logarithm of Constants.phi and divides the result by two, with no lemmas invoked and no tactics applied.
why it matters
This definition supplies the stiffness value used by gcic_stiffness_pos for positivity, by gcic_stiffness_bounds for the interval (0.1152, 0.1167), by mf_temp_eq_six_kappa to equate the mean-field critical temperature to six times κ, and by gcic_thermodynamics_cert to certify the full set of thermodynamic inequalities. It anchors the phi-ladder (T6) to the eight-tick octave and D = 3 setting in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.