cert
plain-language theorem explainer
The declaration cert assembles an explicit instance of the HaberBoschCert structure that witnesses the phi-ladder predictions for the industrial process. A chemist or Recognition Science modeler would cite it to confirm that the operating temperature lies in the observed 400-550 C window, the ratio to minimum temperature equals phi, and the iron-catalyzed barrier reduction is positive. It is formed by a direct structure constructor that supplies four upstream theorems establishing the cost minimum, ratio inequality, range bounds, and barrierpos
Claim. Let HaberBoschCert be the structure whose fields require that the temperature cost vanishes at the minimum temperature, the optimal-to-minimum temperature ratio exceeds one, the optimal temperature in Celsius lies strictly between 400 and 550, and the catalytic barrier ratio is positive. Then cert is the instance of this structure obtained by assigning the theorem haberBoschTempCost_at_min to the first field, optimalTempRatio_gt_one to the second, optimalTemp_in_industrial_range to the third, and catalyticBarrierRatio_pos to the fourth.
background
The module derives Haber-Bosch parameters from the phi-ladder. The structure HaberBoschCert packages four concrete assertions: temperature cost zero when operating temperature equals minimum (via J-cost unit property), optimal temperature ratio greater than one, optimal temperature in the industrial Celsius interval, and positive catalytic barrier ratio. Upstream results include the JCost version of HaberBoschCert requiring five heterogeneous catalysis stages together with a canonical certificate, plus the local theorems catalyticBarrierRatio_pos (proved by linarith on phi_gt_onePointFive), haberBoschTempCost_at_min (proved by unfolding to Jcost_unit0), optimalTemp_in_industrial_range (proved by nlinarith on phi_gt_onePointSixOne), and optimalTempRatio_gt_one (proved by one_lt_phi).
proof idea
The definition is a structure constructor that directly populates the four fields of HaberBoschCert by reference to the named upstream theorems: temp_cost_zero receives haberBoschTempCost_at_min, temp_ratio_gt_one receives optimalTempRatio_gt_one, temp_in_range receives optimalTemp_in_industrial_range, and barrier_pos receives catalyticBarrierRatio_pos. No tactics beyond the structure syntax are used.
why it matters
This definition supplies the concrete witness that closes the structural theorem for the Haber-Bosch process in the phi-ladder tier of the module. It feeds the module-level claim of a zero-sorry result and inherits the five-stage requirement from the JCost HaberBoschCert. The construction realizes the phi fixed-point scaling for temperature and the J-cost reduction of the activation barrier, with the module falsifier being any well-optimized iron-catalyst data placing the optimum outside (400,550) C.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.