sc_prediction
plain-language theorem explainer
Condensed matter theorists modeling superconductivity via Recognition Science cite this result for its concrete prediction that critical temperatures in phi-lattice materials fall between 80 K and 120 K. The claim follows from scaling the J-cost evaluated at the golden ratio by one thousand. The short tactic proof substitutes the closed form for the critical energy, derives the inverse relation from the quadratic identity, and closes both sides of the conjunction with the supplied numerical bounds on phi.
Claim. Let $T_c$ be the phase transition temperature scale defined by $T_c = 1000 E_c$ where the critical energy is $E_c = (phi + phi^{-1})/2 - 1$ and $phi$ is the golden ratio satisfying $phi^2 = phi + 1$. Then $80 < T_c < 120$.
background
The module CondensedMatter.JCostPhaseTransition develops phase transition scales from the J-cost function. J-cost is the map $J(x) = (x + x^{-1})/2 - 1$, and the critical energy is obtained by evaluating this map at the golden ratio. T_critical is the noncomputable definition that multiplies the critical energy by 1000 to obtain a temperature in kelvin. The upstream theorem phi_critical_value supplies the explicit reduction $E_c = (phi + phi^{-1})/2 - 1$, while phi_sq_eq records the quadratic identity $phi^2 = phi + 1$ that is used repeatedly in golden-ratio arithmetic.
proof idea
The proof unfolds T_critical to expose the critical energy, rewrites via phi_critical_value to obtain an explicit expression in phi, then proves the auxiliary identity $phi^{-1} = phi - 1$ by field simplification and nlinarith using phi_sq_eq together with positivity of phi. It imports the tight numerical bounds phi > 1.61 and phi < 1.62, splits the conjunction, and finishes both inequalities by nlinarith.
why it matters
This theorem supplies a falsifiable prediction for superconducting critical temperatures in materials whose lattices admit phi-structured coherence. It directly instantiates the J-uniqueness property from the forcing chain and the phi fixed point, yielding the narrow window 80-120 K that can be checked against cuprate data. The doc-comment links the result to a coherence energy of order phi^{-5} and optimal doping near 1/phi^2. No downstream results yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.