Ignites

formal source

  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