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

ignitionCert

show as:
view Lean formalization →

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.

claimThe 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 in Recognition Science

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.

scope and limits

formal statement (Lean)

  77def ignitionCert : IgnitionCert where
  78  unit_zero := chainCost_zero_at_unit

proof body

Definition body.

  79  reciprocal_symm := chainCost_reciprocal_symm
  80  cost_nonneg := chainCost_nonneg
  81  threshold_band := ignition_threshold_band
  82
  83end
  84end IgnitionThresholdFromJCost
  85end Combustion
  86end IndisputableMonolith

depends on (6)

Lean names referenced from this declaration's body.