chainCost
plain-language theorem explainer
Combustion models define the chain J-cost as the recognition cost applied to the branching-to-termination ratio r. Autoignition researchers would cite this to tie radical propagation thresholds to the universal J-cost function from Recognition Science. The definition is a direct one-line abbreviation that delegates to the core Jcost implementation.
Claim. Let $J$ be the recognition cost function. The combustion-chain J-cost on the branching-to-termination ratio is given by $J(r)$ for $r > 0$.
background
The module models autoignition of a fuel-oxidizer mixture via the recognition cost on the radical-chain branching ratio $r :=$ branching_rate / termination_rate. Below $r=1$ radicals terminate faster than they branch so combustion does not propagate; at $r=1$ the J-cost reaches its minimum but the system is unstable; above $r=1$ the cost rises off zero and propagation follows the phi-ladder. The ignition threshold is identified with the canonical golden-section quantum $J(phi) in (0.11, 0.13)$, the same band that appears in plaque vulnerability, infarction, and dysbiotic disease.
proof idea
The definition is a one-line wrapper that applies Cost.Jcost to the input ratio r.
why it matters
This supplies the cost function used by the Ignites predicate and the IgnitionCert structure, which certify ignition when the cost meets or exceeds the threshold band. It realizes the combustion application of J-uniqueness (T5) from the forcing chain, placing the ignition threshold at the same universal RS quantum as pathology phenomena. The module contributes a zero-sorry formalization of this cross-domain invariant.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.