ignition_threshold_band
plain-language theorem explainer
The theorem establishes that the ignition threshold, defined as J-cost at the golden ratio, satisfies 0.11 < J(φ) < 0.13. Combustion physicists and Recognition Science researchers cite it to place autoignition inside the universal golden-section band shared with pathology thresholds. The proof substitutes the squared algebraic form of J-cost and resolves the resulting inequalities via linear arithmetic on the supplied bounds for φ.
Claim. $0.11 < J(φ) < 0.13$, where $J(x) = (x-1)^2/(2x)$ for $x ≠ 0$ and φ is the golden ratio.
background
The module models autoignition via recognition cost on the radical-chain branching ratio r. Below r = 1 radicals terminate faster than they branch and combustion fails to 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. The ignition threshold is identified with the canonical golden-section quantum J(φ) ∈ (0.11, 0.13), the same band that bounds plaque vulnerability, infarction, Stage-2 hypertension, dysbiotic active disease, and combustion ignition: a single universal RS quantum across pathology and combustion physics.
proof idea
The proof unfolds IgnitionThreshold to Cost.Jcost phi, then rewrites via the lemma Jcost_eq_sq using phi_ne_zero. It establishes positivity of 2*phi from phi_pos, splits the conjunction, rewrites each side with lt_div_iff or div_lt_iff, and closes both inequalities with nlinarith on the bounds phi_gt_onePointSixOne and phi_lt_onePointSixTwo.
why it matters
It supplies the threshold_band field inside the IgnitionCert structure, which certifies that combustion ignition obeys the same J-cost band as other RS phenomena. This directly realizes the module claim that the ignition threshold is the canonical golden-section quantum J(φ) ∈ (0.11, 0.13), linking combustion to the φ-ladder and Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.