pith. machine review for the scientific record. sign in
def definition def or abbrev high

IgnitionThreshold

show as:
view Lean formalization →

The ignition threshold is defined as the J-cost of the golden ratio phi, marking the canonical quantum where radical-chain propagation begins in a fuel-oxidizer mixture. Combustion physicists and Recognition Science researchers cite it when mapping the branching ratio r to the universal phi-ladder band shared with pathology and biology. The declaration is a direct one-line definition that evaluates Cost.Jcost at phi.

claimThe ignition threshold equals $J(phi)$, where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function on positive ratios and $phi$ is the golden ratio.

background

In this module the autoignition of a mixture is controlled by the recognition cost on the branching ratio r = branching_rate / termination_rate. When r < 1 radicals terminate faster than they branch and propagation fails; at r = 1 the J-cost reaches its minimum but the system remains marginal. Above r = 1 the cost rises and follows the phi-ladder, with the threshold fixed at the golden-section quantum J(phi) in (0.11, 0.13).

proof idea

This is a one-line definition that applies Cost.Jcost directly to the constant phi, inheriting non-negativity and symmetry properties from the upstream Cost and ObserverForcing modules.

why it matters in Recognition Science

The definition supplies the numerical threshold consumed by Ignites (a mixture ignites iff chainCost r meets or exceeds the threshold) and by the IgnitionCert structure that records the band property. It places combustion on the same RS quantum used for plaque vulnerability, infarction, and Stage-2 hypertension, consistent with J-uniqueness (T5) and the phi fixed point (T6) in the forcing chain. It also anchors the human rung in AnimalZComplexityBound.

scope and limits

formal statement (Lean)

  48def IgnitionThreshold : ℝ := Cost.Jcost phi

proof body

Definition body.

  49
  50/-- A mixture ignites iff its chain J-cost meets or exceeds the threshold. -/

used by (4)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (7)

Lean names referenced from this declaration's body.