low_temp_bistable

formal source

 374       _ < 2 * ε := by linarith [mul_lt_mul_of_pos_left h_J_over_T (by norm_num : (0 : ℝ) < 2)]
 375
 376/-- At low temperature with J > 0, p → 0 -/
 377theorem low_temp_bistable (trace : LedgerMemoryTrace) (t : ℕ)
 378    (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t)
 379    (h_not_perfect : trace.strength < 1 ∨ t > trace.encoding_tick ∨ trace.ledger_balance ≠ 0) :
 380    ∀ (ε : ℝ), ε > 0 → ∃ T₀ > 0, ∀ sys : RecognitionSystem, sys.TR < T₀ →
 381      equilibrium_remember_prob sys trace t < ε ∨
 382      equilibrium_remember_prob sys trace t > 1 - ε := by
 383  intro ε hε
 384  set J := memory_cost trace t with hJ_def
 385  -- Under h_not_perfect, J > 0 (base cost is positive)
 386  have hJ_pos : 0 < J := by
 387    rw [hJ_def]; unfold memory_cost
 388    have h_disc_pos : 0 < 1 - trace.emotional_weight * (1 - 1/φ) := emotional_discount_pos trace
 389    apply mul_pos h_disc_pos
 390    -- Base cost is positive when h_not_perfect holds
 391    have h_jcost_nonneg : 0 ≤ trace.complexity * Jcost trace.strength :=
 392      mul_nonneg trace.complexity_pos.le (Jcost_nonneg hs)
 393    have h_log_nonneg : 0 ≤ log (1 + (↑t - ↑trace.encoding_tick) / ↑breath_cycle) := by
 394      apply log_nonneg
 395      have hd : 0 ≤ (↑t - ↑trace.encoding_tick : ℝ) := by simp [sub_nonneg, Nat.cast_le, ht]
 396      linarith [div_nonneg hd (le_of_lt breath_cycle_pos)]
 397    have h_abs_nonneg : (0 : ℤ) ≤ |trace.ledger_balance| := abs_nonneg _
 398    have h_int_nonneg : 0 ≤ Jcost (1 + ↑|trace.ledger_balance| / 10) := by
 399      apply Jcost_nonneg
 400      have h_cast_nonneg : (0 : ℝ) ≤ ↑|trace.ledger_balance| := by norm_cast
 401      linarith [div_nonneg h_cast_nonneg (by norm_num : (0 : ℝ) ≤ 10)]
 402    rcases h_not_perfect with h_str | h_t | h_bal
 403    · have h_ne_one : trace.strength ≠ 1 := ne_of_lt h_str
 404      have h_jcost_pos : 0 < Jcost trace.strength := Jcost_pos_of_ne_one trace.strength hs h_ne_one
 405      have h_comp_pos : 0 < trace.complexity * Jcost trace.strength :=
 406        mul_pos trace.complexity_pos h_jcost_pos
 407      linarith