haberBoschTempCost
plain-language theorem explainer
The J-cost of the operating-to-minimum temperature ratio quantifies the energy penalty in Haber-Bosch synthesis under the phi-ladder model. Chemists and Recognition Science modelers cite this definition to link industrial conditions to the underlying J-function. It is realized as the direct application of Jcost to the quotient of the two temperature parameters.
Claim. $Jcost(T_{op}/T_{min})$ where $T_{op}$ denotes the operating temperature and $T_{min}$ the minimum temperature below which reaction kinetics become too slow.
background
The module models the Haber-Bosch process (N2 + 3H2 to 2NH3) via the phi-ladder, with the explicit prediction that the optimal temperature ratio equals phi, yielding T_opt approximately 485 C from a 300 C kinetic threshold. J-cost is the Recognition Science cost function applied to dimensionless ratios, drawn from the imported Cost module and consistent with J(x) = (x + x^{-1})/2 - 1. The upstream T_min definition from BaselineDerivation supplies the vertex count 2^D on the D-dimensional cube (equal to 8 at D=3), providing the discrete foundation that is here scaled to a real temperature threshold.
proof idea
The definition is a one-line wrapper that applies the Jcost function directly to the ratio T_op / T_min.
why it matters
This definition supplies the temperature cost term used in HaberBoschCert to certify that the optimal temperature lies in the industrial range and that the cost vanishes at equality. It realizes the first RS prediction in the module doc-comment for the phi-ladder applied to catalysis. The construction ties into the broader forcing chain through J-uniqueness (T5) and the self-similar fixed point phi (T6).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.