IgnitionCert
plain-language theorem explainer
Combustion modelers cite the IgnitionCert structure to certify that the J-cost on the branching ratio vanishes at unity, is symmetric under reciprocals, is nonnegative for positive ratios, and that the ignition threshold lies in (0.11, 0.13). The structure packages these four properties to witness autoignition governed by recognition cost on the radical chain. It is introduced as a plain structure definition whose fields directly record the required statements.
Claim. A structure $C$ certifying that the J-cost on the branching-to-termination ratio $r$ satisfies $C(1)=0$, $C(r)=C(r^{-1})$ for all $r>0$, $C(r)ge0$ for all $r>0$, and $0.11< I <0.13$ where $I$ is the J-cost evaluated at the golden ratio.
background
The module models autoignition of fuel-oxidizer mixtures via the recognition cost on the radical-chain branching ratio $r$. The chain J-cost is obtained by applying the J-cost function to this ratio. The ignition threshold is defined as the J-cost at the golden ratio and is asserted to lie in the open interval (0.11, 0.13). The module states that this band is the same universal RS quantum that appears in plaque vulnerability, infarction, and dysbiotic disease.
proof idea
The declaration is a structure definition. Its four fields directly encode unit zero, reciprocal symmetry, non-negativity (instantiating the upstream cost-nonneg theorem for recognition events), and the explicit numerical band on the threshold. No tactics, reductions, or lemmas are invoked inside the declaration itself.
why it matters
The certificate is consumed by the downstream ignitionCert definition that assembles a concrete witness from supporting chainCost lemmas. It embeds combustion autoignition inside the Recognition Science framework by equating the threshold with the golden-section J-cost quantum, consistent with the J-uniqueness and phi fixed-point steps of the forcing chain. The module doc notes that the identical band bounds multiple pathology and combustion thresholds.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.