chainCost_zero_at_unit
plain-language theorem explainer
The theorem establishes that the J-cost on the combustion branching ratio vanishes exactly at unit value. Modelers of autoignition thresholds cite it to fix the zero point of the cost function before invoking the phi-ladder for propagation rates. The proof is a one-line wrapper that invokes the unit-zero lemma for the underlying J-cost.
Claim. Let $J(r)$ denote the recognition cost on the radical branching-to-termination ratio $r$. Then $J(1)=0$.
background
In this module the chain cost is defined by applying the J-cost function directly to the branching ratio $r$. The J-cost itself satisfies $J(x)=(x-1)^2/(2x)$ and therefore vanishes at $x=1$, which the module identifies with the marginal-stability point of a radical chain. The local setting is the Recognition Science treatment of autoignition, where cost is zero below threshold, minimal but unstable at $r=1$, and rises above threshold along the phi-ladder.
proof idea
This is a one-line wrapper that applies the Jcost_unit0 lemma from the Cost module, which states Jcost 1 = 0 by direct simplification of the squared-ratio expression.
why it matters
The result supplies the unit_zero field of the downstream ignitionCert definition, which assembles the four canonical properties of the combustion J-cost. It marks the J-cost minimum at the canonical point r=1, the same fixed point that appears in the T5 J-uniqueness step and the phi-ladder mass formula. The module doc-comment notes that the associated J(phi) band (0.11,0.13) unifies combustion ignition with plaque vulnerability and other RS phenomena.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.