ignitionCert
plain-language theorem explainer
The ignitionCert definition packages the zero-at-unit, reciprocal symmetry, non-negativity and threshold-band properties of the recognition cost on branching ratio into the IgnitionCert structure. Combustion modelers working with radical-chain kinetics would cite it to fix the autoignition point inside the universal recognition band. It is a direct record instantiation that applies the four upstream J-cost lemmas without further reduction.
Claim. The combustion ignition certificate asserts that the recognition cost function $C(r)$ on the branching ratio $r$ satisfies $C(1)=0$, $C(r)=C(r^{-1})$ for all $r>0$, $C(r)≥0$ for all $r>0$, and that the ignition threshold lies in the open interval $(0.11,0.13)$.
background
The module treats autoignition as governed by the recognition cost on the radical-chain branching ratio $r$ = branching_rate / termination_rate. Below $r=1$ radicals terminate faster than they branch and combustion fails to propagate; at $r=1$ the cost reaches its global minimum but the system is marginally stable; above $r=1$ the cost rises and propagation follows the phi-ladder. The chainCost function is the J-cost restricted to this ratio, inheriting non-negativity, unit-zero and reciprocal symmetry directly from the Cost module. IgnitionThreshold is defined as the J-cost evaluated at the golden ratio phi and is shown to lie in the canonical band $(0.11,0.13)$ that also bounds plaque vulnerability and Stage-2 hypertension. The upstream cost_nonneg result from ObserverForcing supplies the general non-negativity of any recognition event cost.
proof idea
The definition is a one-line record constructor that supplies chainCost_zero_at_unit to the unit_zero field, chainCost_reciprocal_symm to the reciprocal_symm field, chainCost_nonneg to the cost_nonneg field, and ignition_threshold_band to the threshold_band field.
why it matters
This definition supplies the minimal certificate required by any Recognition Science combustion model. It instantiates the IgnitionCert structure with the J-cost properties that place the ignition threshold inside the universal phi-band $(0.11,0.13)$, the same interval that appears across pathology and the T5 J-uniqueness step of the forcing chain. Because the band is derived from the self-similar fixed point phi forced at T6, the certificate closes the link between microscopic recognition cost and macroscopic ignition without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.