optimalTemp_in_industrial_range
plain-language theorem explainer
The declaration shows that the Recognition Science optimal temperature for Haber-Bosch ammonia synthesis lies strictly between 400 and 550 °C. Industrial chemists checking phi-ladder predictions against plant operating data would cite this bound. The proof splits the conjunction and applies nlinarith directly to the golden-ratio bounds after unfolding the temperature definition.
Claim. $400 < 300 phi < 550$, where $phi$ is the golden ratio and the factor 300 scales the minimum temperature at which kinetics become viable.
background
The module treats the Haber-Bosch process as a structural theorem derived from the phi-ladder. The key definition is optimalTemp_C := 300 * phi, described as the optimal operating temperature (RS): T_min × φ ≈ 485°C. Upstream lemmas supply the tight numerical bounds phi > 1.61 and phi < 1.62. The local theoretical setting is the structural theorem for N₂ + 3H₂ → 2NH₃, which predicts the temperature ratio r_T = phi and places the operating point inside the industrial window.
proof idea
The proof uses the constructor tactic to split the conjunction into two inequalities. It unfolds optimalTemp_C in each goal and invokes nlinarith, first with the lemma phi_gt_onePointSixOne for the lower bound and then with phi_lt_onePointSixTwo for the upper bound.
why it matters
This theorem supplies the temp_in_range field inside the HaberBoschCert structure that aggregates all RS predictions for the process. It directly fills the temperature-range claim stated in the module documentation. In the Recognition framework it confirms the self-similar scaling forced by the phi fixed point (T6) when applied to chemical activation barriers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.