phase_barrier
plain-language theorem explainer
The phase barrier is the J-cost evaluated at 1/2, given explicitly by cosh(ln phi / 2) minus 1 and numerically near 0.029. GCIC thermodynamics work cites this constant when bounding stiffness and critical temperatures in the mean-field model. The definition is a direct one-line expression that invokes the hyperbolic-cosine form of the J function.
Claim. $J̃(1/2) = cosh(ln φ / 2) - 1$
background
The GCIC Phase Thermodynamics module formalizes constants that appear in the response paper “Two Upgrades for the GCIC Paper.” It introduces the phase barrier as the J-cost at argument 1/2. The J-cost satisfies J(x) = cosh(log x) - 1 and obeys the Recognition Composition Law. The definition draws on the Constants structure from LawOfExistence, described as an abstract bundle of CPM constants that includes phi.
proof idea
The definition is a direct one-line expression that applies the identity J(x) = cosh(log x) - 1 to the argument 1/2 using the constant phi.
why it matters
The definition supplies the concrete value of the phase barrier that is invoked by gcic_thermodynamics_cert, phase_barrier_pos, phase_barrier_lower and phase_barrier_upper. It fills the phase-barrier slot required by the GCIC paper’s thermodynamic analysis and links to the J-uniqueness step (T5) in the forcing chain. The surrounding theorems then establish the strict positivity and numerical bounds 0.0287 < phase_barrier < 0.032.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.