combustionCert
plain-language theorem explainer
This definition assembles the CombustionCert structure by supplying the five-regime cardinality, the vanishing J-cost at equivalence ratio 1, and strict positivity of J-cost for all other positive ratios. A physicist working on flame regimes or equivalence-ratio dependence in Recognition Science would cite it as the canonical certification that combustion follows the J-cost model. The construction is a direct field-by-field assignment from three upstream theorems.
Claim. The combustion certificate is the structure asserting that the set of combustion regimes has cardinality 5, that the J-cost function satisfies $J(1)=0$, and that $J(r)>0$ for every $r>0$ with $r≠1$.
background
The CombustionFromJCost module derives combustion physics from the J-cost function on the fuel-air equivalence ratio. Stoichiometric combustion occurs at ratio 1 where J-cost vanishes, corresponding to recognition equilibrium; all other ratios incur positive J-cost. The module enumerates five regimes (lean deflagration, stoichiometric, rich deflagration, detonation, distributed reaction zone) and equates their count to the configuration dimension 5.
proof idea
The definition is a direct structure constructor that populates the three fields of CombustionCert by referencing the theorems combustionRegimeCount, stoichiometric_equilibrium, and off_stoichiometric_cost.
why it matters
This supplies the concrete CombustionCert instance that certifies the five-regime combustion model inside the Recognition Science framework. It realizes the B11 claim that combustion regimes number five, consistent with the eight-tick octave and the extension of spatial dimension D=3 to configuration dimension 5. The module closes with zero sorrys after deriving the J-cost properties from the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.