IndisputableMonolith.Combustion.IgnitionThresholdFromJCost

   1import Mathlib
   2import IndisputableMonolith.Cost
   3import IndisputableMonolith.Constants
   4
   5/-!
   6# Combustion Ignition Threshold from J-Cost
   7
   8The autoignition of a fuel-oxidizer mixture is governed by the
   9recognition cost on the radical-chain branching ratio
  10`r := branching_rate / termination_rate`. Below `r = 1` (radicals
  11terminate faster than they branch) combustion does not propagate. At
  12`r = 1` the system is at the J-cost minimum but unstable; combustion is
  13marginal. Above `r = 1`, J-cost rises off-zero and the propagation rate
  14follows the φ-ladder.
  15
  16The ignition threshold corresponds to the canonical golden-section
  17quantum `J(φ) ∈ (0.11, 0.13)`. This is the same band that bounds plaque
  18vulnerability, infarction, Stage-2 hypertension, dysbiotic active
  19disease, and now combustion ignition: a single universal RS quantum
  20across pathology and combustion physics.
  21
  22Lean status: 0 sorry, 0 axiom.
  23-/
  24
  25namespace IndisputableMonolith
  26namespace Combustion
  27namespace IgnitionThresholdFromJCost
  28
  29open Constants Cost
  30
  31noncomputable section
  32
  33/-- Combustion-chain J-cost on the branching/termination ratio. -/
  34def chainCost (r : ℝ) : ℝ := Cost.Jcost r
  35
  36theorem chainCost_zero_at_unit : chainCost 1 = 0 := Cost.Jcost_unit0
  37
  38theorem chainCost_reciprocal_symm {r : ℝ} (hr : 0 < r) :
  39    chainCost r = chainCost r⁻¹ := Cost.Jcost_symm hr
  40
  41theorem chainCost_nonneg {r : ℝ} (hr : 0 < r) : 0 ≤ chainCost r :=
  42  Cost.Jcost_nonneg hr
  43
  44theorem chainCost_pos_off_unit {r : ℝ} (hr : 0 < r) (hne : r ≠ 1) :
  45    0 < chainCost r := Cost.Jcost_pos_of_ne_one r hr hne
  46
  47/-- Ignition threshold: the canonical golden-section J-cost quantum. -/
  48def IgnitionThreshold : ℝ := Cost.Jcost phi
  49
  50/-- A mixture ignites iff its chain J-cost meets or exceeds the threshold. -/
  51def Ignites (r : ℝ) : Prop := IgnitionThreshold ≤ chainCost r
  52
  53/-- Ignition threshold lies in the canonical band. -/
  54theorem ignition_threshold_band :
  55    0.11 < IgnitionThreshold ∧ IgnitionThreshold < 0.13 := by
  56  unfold IgnitionThreshold
  57  have hphi_ne : phi ≠ 0 := Constants.phi_ne_zero
  58  rw [Cost.Jcost_eq_sq hphi_ne]
  59  have h_lo : (1.61 : ℝ) < phi := Constants.phi_gt_onePointSixOne
  60  have h_hi : phi < (1.62 : ℝ) := Constants.phi_lt_onePointSixTwo
  61  have hpos : (0 : ℝ) < 2 * phi := by
  62    have : (0 : ℝ) < phi := Constants.phi_pos
  63    linarith
  64  refine ⟨?lo, ?hi⟩
  65  · rw [lt_div_iff₀ hpos]
  66    nlinarith [h_lo, h_hi]
  67  · rw [div_lt_iff₀ hpos]
  68    nlinarith [h_lo, h_hi]
  69
  70structure IgnitionCert where
  71  unit_zero : chainCost 1 = 0
  72  reciprocal_symm : ∀ {r : ℝ}, 0 < r → chainCost r = chainCost r⁻¹
  73  cost_nonneg : ∀ {r : ℝ}, 0 < r → 0 ≤ chainCost r
  74  threshold_band : 0.11 < IgnitionThreshold ∧ IgnitionThreshold < 0.13
  75
  76/-- Combustion ignition certificate. -/
  77def ignitionCert : IgnitionCert where
  78  unit_zero := chainCost_zero_at_unit
  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
  87