chainCost

formal source

  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⟩