phase_barrier_lower
plain-language theorem explainer
The theorem establishes a numerical lower bound of 0.0287 on the GCIC phase barrier height J̃(1/2). Researchers calibrating phase transitions and critical temperatures in Recognition Science thermodynamics cite this anchor when fixing the stiffness scale. The proof unfolds the barrier definition, invokes the lemma that log φ exceeds 0.48 to bound the cosh argument above 0.24, applies the quadratic lower bound cosh x ≥ 1 + x²/2, and closes the inequality with linear arithmetic.
Claim. $0.0287 ≤ J̃(1/2)$, where $J̃(1/2) := cosh((log φ)/2) - 1$ and φ denotes the golden ratio.
background
The GCIC thermodynamics module formalizes numerical constants for stiffness, barrier height, and phase structure drawn from the GCIC Response paper. The phase barrier is the modified J-cost evaluated at argument 1/2, with J(x) = cosh(log x) - 1 the Recognition Science cost function; here the argument is scaled by log φ so that J̃(1/2) = cosh((log φ)/2) - 1. The module imports the quadratic lower bound cosh x ≥ 1 + x²/2 (valid for all real x) and the numerical fact log φ > 0.48.
proof idea
The tactic proof first unfolds the definition of phase_barrier. It obtains log φ > 0.48 from the lemma log_phi_gt_048, then uses monotonicity of cosh on the non-negative reals to replace the argument log φ/2 by the smaller value 0.24. The quadratic lower bound is applied at 0.24 to produce cosh(0.24) ≥ 1.0288. Linear arithmetic assembles the chain 0.0287 ≤ cosh(0.24) - 1 ≤ cosh(log φ/2) - 1.
why it matters
The bound supplies the concrete lower anchor for the phase barrier that appears in the GCIC stiffness and critical-temperature calculations. It sits inside the thermodynamic layer of Recognition Science that follows the eight-tick octave and phi-ladder constructions, providing a numerically stable floor for the energy scale separating phases. The GCIC Response paper invokes such bounds when upgrading the model; the present theorem closes the lower half of the interval estimate for J̃(1/2).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.