off_stoichiometric_cost
plain-language theorem explainer
Off-stoichiometric combustion incurs positive J-cost. Combustion modelers would cite this when showing that rich or lean mixtures carry positive deviation cost away from the stoichiometric point. The proof is a one-line wrapper that invokes the general positivity lemma for the J-cost function.
Claim. For any real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < Jcost(r)$.
background
The J-cost function from the Cost module vanishes exactly at equilibrium (r = 1) and is strictly positive elsewhere for r > 0. The upstream lemma Jcost_pos_of_ne_one proves this by rewriting Jcost via Jcost_eq_sq as a square divided by a positive term, then applying sq_pos_of_ne_zero. The module CombustionFromJCost embeds this fact into combustion physics: the fuel-air equivalence ratio equals 1 at stoichiometric equilibrium (J = 0), while off-stoichiometric regimes (r ≠ 1) produce positive J-cost. The module states that five canonical regimes arise from configDim D = 5.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module directly to the hypotheses hr and hne.
why it matters
This theorem supplies the off_stoich_cost field inside the CombustionCert definition, which bundles five_regimes, stoichiometric_equilibrium, and off_stoichiometric_cost. It completes the step showing non-stoichiometric mixtures carry positive J-cost, aligning with the framework derivation of combustion from the J-function where peak efficiency occurs at J = 0. It supports the five-regime count without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.