low_temp_bistable

proof body

Tactic-mode proof.

 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
 408    · have h_log_pos : 0 < log (1 + (↑t - ↑trace.encoding_tick) / ↑breath_cycle) := by
 409        apply log_pos
 410        have hd : 0 < (↑t - ↑trace.encoding_tick : ℝ) := by
 411          simp only [sub_pos, Nat.cast_lt]; exact h_t
 412        linarith [div_pos hd breath_cycle_pos]
 413      linarith
 414    · have h_bal_pos : (0 : ℤ) < |trace.ledger_balance| := abs_pos.mpr h_bal
 415      have h_cast_pos : (0 : ℝ) < ↑|trace.ledger_balance| := by exact_mod_cast h_bal_pos
 416      have h_arg_pos : (0 : ℝ) < (1 : ℝ) + (↑|trace.ledger_balance| : ℝ) / (10 : ℝ) := by
 417        have hd : (0 : ℝ) < (↑|trace.ledger_balance| : ℝ) / (10 : ℝ) := div_pos h_cast_pos (by norm_num)
 418        linarith
 419      have h_arg_ne_one : (1 : ℝ) + (↑|trace.ledger_balance| : ℝ) / (10 : ℝ) ≠ (1 : ℝ) := by
 420        have hd : (0 : ℝ) < (↑|trace.ledger_balance| : ℝ) / (10 : ℝ) := div_pos h_cast_pos (by norm_num)
 421        linarith
 422      have h_int_pos : 0 < Jcost (1 + ↑|trace.ledger_balance| / 10) :=
 423        Jcost_pos_of_ne_one _ h_arg_pos h_arg_ne_one
 424      linarith
 425  -- Choose T₀ small enough: for J > 0, exp(-J/T) → 0 as T → 0+
 426  -- We need p = e/(e+1) < ε where e = exp(-J/T) → 0
 427  -- For e < ε/(1-ε) (assuming ε < 1), we have p < ε
 428  -- exp(-J/T) < ε/(1-ε) when -J/T < log(ε/(1-ε)), i.e., T < J/(-log(ε/(1-ε)))
 429  -- For ε ≥ 1, just take T small enough that e < 1
 430  use min 1 (J / (|log (ε / 2)| + 1))
 431  constructor
 432  · apply lt_min_iff.mpr
 433    constructor
 434    · norm_num
 435    · apply div_pos hJ_pos
 436      linarith [abs_nonneg (log (ε / 2))]
 437  · intro sys hT
 438    have hT_pos : 0 < sys.TR := sys.TR_pos
 439    left -- We'll show p < ε (since J > 0)
 440    unfold equilibrium_remember_prob; simp only
 441    set e := exp (-J / sys.TR) with he_def
 442    have he_pos : 0 < e := exp_pos _
 443    have h_denom_pos : 0 < e + 1 := by linarith
 444    -- p = e/(e+1), and e is very small for small T
 445    -- Need: e/(e+1) < ε
 446    -- Since e/(e+1) < e (for e > 0), it suffices to show e < ε
 447    have h_p_lt_e : e / (e + 1) < e := by
 448      rw [div_lt_iff₀ h_denom_pos]
 449      -- Need: e < e * (e + 1) = e*e + e  ⟺  0 < e*e (since e > 0)
 450      have h1 : e * (e + 1) = e * e + e := by ring
 451      rw [h1]
 452      have h2 : 0 < e * e := mul_pos he_pos he_pos
 453      linarith
 454    apply lt_of_lt_of_le h_p_lt_e
 455    -- Need e ≤ ε, i.e., exp(-J/T) ≤ ε
 456    -- -J/T < log ε when T < J/(-log ε) (for ε < 1)
 457    -- Our bound T < J/(|log(ε/2)|+1) ensures exp(-J/T) is small
 458    -- For now, use the structure: with small T and J > 0, exp(-J/T) → 0
 459    have hT_small : sys.TR < J / (|log (ε / 2)| + 1) :=
 460      lt_of_lt_of_le hT (min_le_right _ _)
 461    have h_arg_large : -J / sys.TR < log ε := by
 462      have h_denom_pos' : 0 < |log (ε / 2)| + 1 := by linarith [abs_nonneg (log (ε / 2))]
 463-- ... 47 more lines elided ...