Ignites
plain-language theorem explainer
A mixture ignites precisely when the J-cost of its branching-to-termination ratio r meets or exceeds the golden-section threshold J(φ). Combustion physicists cite the predicate when modeling autoignition criteria inside the recognition-cost framework. The declaration is a direct definition that equates the ignition condition to the inequality between the precomputed threshold and the chain-cost function.
Claim. A fuel-oxidizer mixture ignites if and only if $J(r) ≥ J(φ)$, where $r$ is the branching-to-termination ratio and $J$ is the recognition J-cost function with threshold $J(φ)$ the canonical golden-section quantum.
background
The module treats autoignition as governed by recognition cost on the radical-chain ratio $r :=$ branching_rate / termination_rate. Below $r=1$ radicals terminate faster than they branch and combustion does not propagate; at $r=1$ the system sits at the J-cost minimum but is unstable; above $r=1$ J-cost rises and propagation follows the φ-ladder. IgnitionThreshold is defined as Cost.Jcost φ, the same canonical band (0.11,0.13) that appears in plaque vulnerability and Stage-2 hypertension. chainCost r is defined identically as Cost.Jcost r, so the predicate simply compares the two evaluations.
proof idea
Direct definition: Ignites r holds exactly when the precomputed IgnitionThreshold is ≤ chainCost r. No lemmas or tactics are invoked beyond the sibling definitions of chainCost and IgnitionThreshold.
why it matters
The definition embeds combustion inside Recognition Science by identifying the ignition threshold with the universal J(φ) quantum that also bounds pathology. It supplies the predicate used by downstream objects such as IgnitionCert and ignition_threshold_band, closing the link between the φ-ladder (T6) and physical propagation rates. The construction keeps the same numerical band across domains without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.