CombustionCert
plain-language theorem explainer
CombustionCert defines a certificate structure asserting exactly five combustion regimes, vanishing J-cost at equivalence ratio one, and strictly positive J-cost for all other positive ratios. Researchers modeling flame efficiency from the J-cost function would cite this to anchor the stoichiometric baseline. The structure is a bare definition whose fields are supplied by a downstream constructor assembling the regime count and cost lemmas.
Claim. A structure certifying combustion physics from the J-cost function, requiring that the set of combustion regimes has cardinality five, that the J-cost equals zero at equivalence ratio one, and that the J-cost is strictly positive for every positive equivalence ratio different from one.
background
In the Recognition Science treatment of combustion the J-cost function quantifies the energetic penalty of a fuel-air equivalence ratio r. The module enumerates five canonical regimes (lean deflagration, stoichiometric, rich deflagration, detonation, distributed reaction zone) that arise as the configuration dimension for the process. The upstream inductive definition of CombustionRegime lists these five cases and carries the Fintype instance used to obtain the cardinality claim.
proof idea
The declaration is a structure definition with no proof body. It simply declares the three fields. The downstream definition combustionCert supplies the concrete values by invoking combustionRegimeCount for the cardinality, stoichiometric_equilibrium for the zero at ratio one, and off_stoichiometric_cost for the positivity condition.
why it matters
CombustionCert supplies the interface that lets the J-cost model reproduce the observed structure of combustion regimes and the location of peak efficiency. It is instantiated by combustionCert and thereby feeds any subsequent theorem that invokes the certified properties. Within the framework it realizes the claim that five regimes follow from the configuration dimension and that the J-cost vanishes at the self-similar fixed point r=1.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.