J_bit_pos

formal source

  52noncomputable def J_bit : ℝ := Real.log φ
  53
  54/-- J_bit is positive (φ > 1 → ln φ > 0) -/
  55lemma J_bit_pos : 0 < J_bit := by
  56  unfold J_bit φ
  57  exact Real.log_pos Constants.one_lt_phi
  58
  59/-! ## Recognition Cost Model -/
  60
  61/-- Recognition cost for scale ratio x: J(x) = ½(x + 1/x) - 1 -/
  62noncomputable def J (x : ℝ) : ℝ := Cost.Jcost x
  63
  64/-- J is minimized at x = 1 with J(1) = 0 -/
  65lemma J_unit_zero : J 1 = 0 := Cost.Jcost_unit0
  66
  67/-- J is nonnegative for positive arguments -/
  68lemma J_nonneg {x : ℝ} (hx : 0 < x) : 0 ≤ J x := by
  69  unfold J
  70  have : Cost.Jcost x = (x - 1)^2 / (2 * x) := by
  71    unfold Cost.Jcost
  72    have hne : x ≠ 0 := ne_of_gt hx
  73    field_simp [hne]
  74    ring
  75  rw [this]
  76  exact div_nonneg (sq_nonneg _) (by linarith)
  77
  78/-! ## Stellar Configuration -/
  79
  80/-- A stellar configuration specifies the scale ratios for emission and storage -/
  81structure StellarConfig where
  82  /-- Scale ratio for photon emission events -/
  83  r_emit : ℝ
  84  /-- Scale ratio for mass storage events -/
  85  r_store : ℝ