combustionRegimeCount
plain-language theorem explainer
The theorem asserts that the Recognition Science model admits exactly five combustion regimes. Researchers modeling flame propagation or engine efficiency would cite this cardinality when mapping J-cost to equivalence ratio regimes. The proof proceeds by a single decide tactic that computes the cardinality of the inductive type enumerating the regimes.
Claim. The set of combustion regimes has cardinality five: $|$ {lean deflagration, stoichiometric equilibrium, rich deflagration, detonation, distributed reaction zone} $| = 5$.
background
In the Combustion Physics from J-Cost module, combustion is rapid oxidation releasing heat and light, with adiabatic flame temperature depending on fuel-air equivalence ratio. The RS derivation sets peak efficiency at stoichiometric point where J-cost vanishes, matching equilibrium. Five regimes are identified as the configurations with dimension five.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. CombustionRegime derives Fintype from its five constructors, so decide evaluates the finite cardinality directly.
why it matters
This theorem supplies the five_regimes field to the CombustionCert definition, which certifies the combustion model. It realizes configDim D = 5 for combustion regimes in the RS framework and links to the upstream equilibrium result that Jcost 1 equals zero. It closes the enumeration needed for downstream certification of stoichiometric and off-stoichiometric costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.