optimalTempRatio_gt_one
plain-language theorem explainer
The theorem establishes that the optimal operating-to-minimum temperature ratio in the Recognition Science model of Haber-Bosch ammonia synthesis strictly exceeds one. Process chemists validating predicted operating points near 485°C against industrial 450-500°C data would cite this inequality. The proof is a direct term application of the established golden-ratio inequality.
Claim. Let $r_T$ denote the optimal operating-to-minimum temperature ratio, defined by $r_T = phi$. Then $1 < r_T$.
background
In the Recognition Science treatment of the Haber-Bosch process the minimum temperature marks the kinetic threshold below which rates become impractically slow, while the optimal temperature is obtained by scaling that threshold by the golden ratio. The module sets the ratio exactly to phi and draws T_min from the baseline derivation as the cube-vertex count at spatial dimension 3. Upstream, the definition optimalTempRatio fixes the ratio to phi while the lemma one_lt_phi proves phi exceeds 1 by algebraic comparison of square roots and bounds.
proof idea
The proof is a one-line term wrapper that directly applies the lemma one_lt_phi.
why it matters
This supplies the temperature-ratio field of the HaberBoschCert certificate, which aggregates the zero-cost condition at minimum temperature, the ratio inequality, the industrial-range check, and the positive barrier ratio. It realizes the Tier B10 structural prediction that optimal temperature equals T_min times phi, consistent with the self-similar fixed point forced at T6. The parent cert is the top-level object used to certify the entire RS-derived operating point against the module falsifier of temperatures outside 400-550°C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.