gcic_stiffness_bounds
plain-language theorem explainer
The GCIC stiffness constant satisfies the strict numerical bounds 0.1152 < κ < 0.1167. Researchers formalizing phase thermodynamics in the GCIC model would cite this interval when pinning down the stiffness parameter for thermodynamic calculations. The proof is a short term-mode argument that unfolds the definition of gcic_stiffness, pulls in the established interval bounds on log φ, and closes both sides of the conjunction via nlinarith applied to squared deviation terms.
Claim. $0.1152 < κ < 0.1167$, where $κ$ is the GCIC stiffness constant expressed in terms of the logarithm of the golden ratio.
background
The module formalizes key numerical constants for GCIC phase thermodynamics, including stiffness and the phase barrier. The stiffness κ is defined via the golden ratio φ (with log φ appearing explicitly after unfolding), consistent with the J-cost J(x) = cosh(log x) - 1 used throughout Recognition Science. The upstream Constants structure from CPM.LawOfExistence bundles the core parameters Knet, Cproj, Ceng, and Cdisp with the non-negativity axiom on Knet.
proof idea
The proof unfolds gcic_stiffness to expose its dependence on log φ. It obtains the lower bound log φ > 0.48 via log_phi_gt_048 and the upper bound log φ < 0.483 via log_phi_lt_0483. The constructor splits the conjunction; nlinarith then closes each inequality using the non-negativity of the squares (log φ - 0.48)^2, (log φ - 0.483)^2, and (log φ)^2.
why it matters
This supplies a concrete numerical interval for the stiffness constant in the GCIC phase structure, directly supporting the constants formalized from the GCIC Response paper. It sits inside the Recognition framework via the golden-ratio logarithm that enters the J-cost and the forcing chain (T5–T6). No downstream results currently depend on it, leaving open its later use in derivations such as critical temperatures or phase-barrier relations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.