gcic_stiffness_pos
plain-language theorem explainer
The GCIC stiffness constant defined as (ln φ)^2 / 2 is strictly positive. Researchers formalizing phase thermodynamics in the GCIC model cite this to secure the sign of the stiffness parameter. The proof unfolds the definition then applies div_pos and pow_pos to the positive logarithm of φ.
Claim. $0 < ( (ln φ)^2 ) / 2$ where φ denotes the golden ratio with 1 < φ.
background
The module formalizes GCIC phase thermodynamics, covering stiffness, barrier, and phase structure as key constants from the GCIC Response paper. The stiffness constant is introduced via the definition (Real.log φ)^2 / 2. Upstream, the lemma one_lt_phi establishes 1 < φ, which forces the logarithm to be positive. The Constants structure from CPM.LawOfExistence bundles related real-valued parameters with nonnegativity conditions.
proof idea
The term proof unfolds the stiffness definition to expose the quotient. It applies div_pos, discharging the positive denominator via norm_num, then invokes pow_pos on the square of the positive value supplied by Real.log_pos applied to one_lt_phi.
why it matters
This result supplies the first conjunct in gcic_thermodynamics_cert, which bundles positivity of stiffness, phase barrier, and critical temperature with a uniform convexity bound. It completes the sign requirements for the GCIC thermodynamics constants in the formalization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.