phase_barrier_upper
plain-language theorem explainer
The declaration proves an upper bound of 0.032 on the GCIC phase barrier J̃(1/2). Researchers working on mean-field critical temperatures and phase structure in the GCIC Response paper would cite this numerical control. The proof applies the cosh quadratic remainder estimate to the argument log phi over 2, then tightens the resulting quadratic and quartic terms with explicit numerical comparisons.
Claim. $J̃(1/2) < 0.032$, where $J̃(1/2) := cosh(log φ / 2) - 1$ and φ denotes the golden ratio.
background
The GCIC Thermodynamics module formalizes stiffness, barrier, and phase structure constants drawn from the GCIC Response paper. The phase barrier is the J-cost at half-log-phi, with J(x) = cosh(log x) - 1 the standard Recognition Science functional. Upstream, the cosh_quadratic_bound theorem states: For |x| < 1, the Taylor remainder satisfies |cosh x - 1 - x²/2| ≤ x⁴/20. The lemma log phi < 0.483 supplies the concrete numerical input.
proof idea
The tactic proof unfolds phase_barrier, establishes positivity and the bound log phi / 2 < 0.242 from log_phi_lt_0483, verifies |x| < 1, then applies cosh_quadratic_bound. Separate calc blocks bound the square below 0.0586 and the fourth power below 0.00344. A final ring-plus-linarith chain adds the remainder term and shows the total is less than 0.032.
why it matters
The bound supplies a concrete numerical anchor for phase-barrier estimates that support mean-field critical temperature calculations among the module siblings. It instantiates the J-uniqueness step (T5) of the forcing chain inside the GCIC thermodynamics setting. The result closes a numerical gap in the phase-structure analysis without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.