phase_barrier_pos
plain-language theorem explainer
The theorem proves that the phase barrier, given by cosh(log φ / 2) - 1, is strictly positive. Workers on GCIC phase thermodynamics cite it to confirm a positive energy barrier at the half point. The proof reduces the claim to the known inequality 1 < cosh x for x ≠ 0 after verifying the argument is nonzero via φ > 1.
Claim. $0 < J̃(1/2)$ where $J̃(1/2) := cosh(ln φ / 2) - 1$ and φ is the golden ratio.
background
The GCIC Phase Thermodynamics module formalizes key constants from the GCIC Response paper 'Two Upgrades for the GCIC Paper' (Feb 2026). The phase barrier is introduced via the definition phase_barrier := Real.cosh (Real.log Constants.phi / 2) - 1, which equals J̃(1/2) ≈ 0.029 in the Recognition framework. Upstream, one_lt_phi establishes that the golden ratio φ satisfies 1 < φ, which is used to ensure the logarithm is positive and nonzero. The Constants structure from CPM.LawOfExistence provides the abstract bundle of CPM constants.
proof idea
Unfold the definition of phase_barrier. Establish that Real.log Constants.phi / 2 ≠ 0 by div_ne_zero and Real.log_ne_zero_of_pos_of_ne_one, relying on Constants.phi_pos and one_lt_phi. Apply Real.one_lt_cosh.mpr to obtain 1 < Real.cosh (Real.log Constants.phi / 2). Conclude positivity by linarith.
why it matters
This positivity result is invoked in gcic_thermodynamics_cert to certify the full set of thermodynamic inequalities including 0 < phase_barrier. It supports the phase structure analysis in the GCIC paper by ensuring the barrier is positive, consistent with the Recognition Science forcing chain where phi is the self-similar fixed point. No open questions are directly addressed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.