phi_critical_value
plain-language theorem explainer
The theorem equates the critical energy scale at the golden ratio to the explicit J-cost expression (phi plus phi inverse over 2 minus 1). Condensed matter researchers modeling phase transitions in phi-structured lattices cite this when fixing the energy gap for superconducting predictions. The proof is a direct unfolding of the two definitions followed by reflexivity.
Claim. The critical energy scale at the golden ratio satisfies $E_c = (phi + phi^{-1})/2 - 1$.
background
In the JCostPhaseTransition module the J-cost function is defined as J(x) := (x + x^{-1})/2 - 1, matching the canonical form from J-uniqueness in the forcing chain. The critical energy is introduced as the direct application J_cost(phi), where phi denotes the self-similar fixed point. This supplies the algebraic energy scale for phase-transition analysis in condensed matter, resting on the upstream J_cost definition.
proof idea
The proof is a one-line wrapper that unfolds phi_critical_energy and J_cost then applies reflexivity.
why it matters
This supplies the closed-form value required by the numeric bounds theorem phi_critical_numeric and the falsifiable superconducting prediction sc_prediction (T_c between 80 and 120 K for phi-lattice materials). It instantiates J-uniqueness (T5) and the phi fixed point (T6) from the unified forcing chain at the condensed-matter level, closing the algebraic step before numeric evaluation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.