IndisputableMonolith.Thermodynamics.MemoryLedger
IndisputableMonolith/Thermodynamics/MemoryLedger.lean · 577 lines · 24 declarations
show as:
view math explainer →
1import Mathlib
2import IndisputableMonolith.Constants
3import IndisputableMonolith.Thermodynamics.RecognitionThermodynamics
4import IndisputableMonolith.Thermodynamics.FreeEnergyMonotone
5import IndisputableMonolith.Foundation.PhiForcing
6import IndisputableMonolith.Cost
7
8/-!
9# Memory Ledger: Dynamics of Learning
10
11This module formalizes memory as a **thermodynamic system** governed by Recognition Science
12principles. Memory becomes a solvable physics problem: **retention vs. free-energy decay**.
13
14## Proof Status
15- `memory_cost_nonneg`: PROVEN ✅
16- `emotional_reduces_cost`: PROVEN ✅
17- `forgetting_decreases`: PROVEN ✅
18- `emotional_forgets_slower`: PROVEN ✅
19- `high_temp_maximizes_entropy`: PROVEN ✅
20- `low_temp_bistable`: PROVEN ✅
21- `learning_rate_nonneg`: PROVEN ✅
22- `learning_compounds`: PROVEN ✅
23
24**All thermodynamic memory theorems are now fully proven with no sorries!**
25-/
26
27namespace IndisputableMonolith
28namespace Thermodynamics
29namespace MemoryLedger
30
31open Real
32open Cost
33open Foundation.PhiForcing
34open Filter Topology
35
36/-! ## Memory Trace Structure -/
37
38structure LedgerMemoryTrace where
39 id : ℕ
40 complexity : ℝ
41 complexity_pos : 0 < complexity
42 emotional_weight : ℝ
43 emotional_bounded : 0 ≤ emotional_weight ∧ emotional_weight ≤ 1
44 encoding_tick : ℕ
45 strength : ℝ
46 strength_bounded : 0 ≤ strength ∧ strength ≤ 1
47 consolidated : Bool
48 ledger_balance : ℤ
49
50noncomputable def base_decay_rate : ℝ := 1 / φ
51
52theorem base_decay_rate_pos : 0 < base_decay_rate := div_pos zero_lt_one phi_pos
53
54def working_memory_window : ℕ := 8
55def breath_cycle : ℕ := 1024
56
57theorem breath_cycle_pos : 0 < (breath_cycle : ℝ) := by unfold breath_cycle; norm_num
58
59/-! ## Memory J-Cost -/
60
61noncomputable def memory_cost (trace : LedgerMemoryTrace) (current_tick : ℕ) : ℝ :=
62 let time_elapsed := (current_tick - trace.encoding_tick : ℝ)
63 let complexity_cost := trace.complexity * Jcost trace.strength
64 let time_cost := log (1 + time_elapsed / breath_cycle)
65 let interference_cost := Jcost (1 + |trace.ledger_balance| / 10)
66 let emotional_discount := 1 - trace.emotional_weight * (1 - 1/φ)
67 emotional_discount * (complexity_cost + time_cost + interference_cost)
68
69/-- Emotional discount is always positive (0 < 1 - w*(1 - 1/φ)) -/
70lemma emotional_discount_pos (trace : LedgerMemoryTrace) :
71 0 < 1 - trace.emotional_weight * (1 - 1/φ) := by
72 have h1 : 1 < φ := phi_gt_one
73 have h2 : 0 < φ := phi_pos
74 have h2' : 0 < 1/φ := div_pos one_pos h2
75 have h3 : 1/φ < 1 := by rw [div_lt_one h2]; exact h1
76 have h4 : 0 < 1 - 1/φ := by linarith
77 have h4' : 1 - 1/φ < 1 := by linarith
78 have hw := trace.emotional_bounded
79 have h5 : trace.emotional_weight * (1 - 1/φ) < 1 := by
80 calc trace.emotional_weight * (1 - 1/φ)
81 ≤ 1 * (1 - 1/φ) := mul_le_mul_of_nonneg_right hw.2 (le_of_lt h4)
82 _ = 1 - 1/φ := one_mul _
83 _ < 1 := h4'
84 linarith
85
86theorem memory_cost_nonneg (trace : LedgerMemoryTrace) (t : ℕ)
87 (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
88 0 ≤ memory_cost trace t := by
89 unfold memory_cost; dsimp only
90 apply mul_nonneg (le_of_lt (emotional_discount_pos trace))
91 -- Each term is nonnegative: complexity*Jcost ≥ 0, log(1+...) ≥ 0, Jcost(...) ≥ 0
92 -- Sum of nonnegatives is nonnegative
93 have h1 : 0 ≤ trace.complexity * Jcost trace.strength :=
94 mul_nonneg trace.complexity_pos.le (Jcost_nonneg hs)
95 have h2 : 0 ≤ log (1 + (↑t - ↑trace.encoding_tick) / ↑breath_cycle) := by
96 apply log_nonneg
97 have hd : 0 ≤ (↑t - ↑trace.encoding_tick : ℝ) := by simp [sub_nonneg, Nat.cast_le, ht]
98 linarith [div_nonneg hd (le_of_lt breath_cycle_pos)]
99 have h3 : 0 ≤ Jcost (1 + (↑|trace.ledger_balance| : ℝ) / 10) := by
100 apply Jcost_nonneg
101 -- |trace.ledger_balance| ≥ 0 as an integer, so its cast to ℝ is also ≥ 0
102 have h_abs_nonneg : (0 : ℤ) ≤ |trace.ledger_balance| := abs_nonneg _
103 have h_cast_nonneg : (0 : ℝ) ≤ ↑|trace.ledger_balance| := by norm_cast
104 linarith [div_nonneg h_cast_nonneg (by norm_num : (0 : ℝ) ≤ 10)]
105 -- Sum of nonnegative terms is nonnegative
106 exact add_nonneg (add_nonneg h1 h2) h3
107
108/-- Emotional memories have lower cost -/
109theorem emotional_reduces_cost (trace1 trace2 : LedgerMemoryTrace) (t : ℕ)
110 (h_same : trace1.complexity = trace2.complexity ∧
111 trace1.strength = trace2.strength ∧
112 trace1.encoding_tick = trace2.encoding_tick ∧
113 trace1.ledger_balance = trace2.ledger_balance)
114 (h_more : trace1.emotional_weight > trace2.emotional_weight)
115 (hs1 : trace1.strength > 0) (_hs2 : trace2.strength > 0)
116 (ht : trace1.encoding_tick ≤ t)
117 (h_not_perfect : trace1.strength < 1 ∨ t > trace1.encoding_tick ∨ trace1.ledger_balance ≠ 0) :
118 memory_cost trace1 t < memory_cost trace2 t := by
119 unfold memory_cost; simp only
120 -- The base costs are equal since complexity, strength, encoding_tick, ledger_balance are equal
121 have h_complexity_eq : trace1.complexity = trace2.complexity := h_same.1
122 have h_strength_eq : trace1.strength = trace2.strength := h_same.2.1
123 have h_tick_eq : trace1.encoding_tick = trace2.encoding_tick := h_same.2.2.1
124 have h_balance_eq : trace1.ledger_balance = trace2.ledger_balance := h_same.2.2.2
125 -- Base cost is the same
126 have h_base_eq : trace1.complexity * Jcost trace1.strength + log (1 + (↑t - ↑trace1.encoding_tick) / ↑breath_cycle) + Jcost (1 + ↑|trace1.ledger_balance| / 10) =
127 trace2.complexity * Jcost trace2.strength + log (1 + (↑t - ↑trace2.encoding_tick) / ↑breath_cycle) + Jcost (1 + ↑|trace2.ledger_balance| / 10) := by
128 rw [h_complexity_eq, h_strength_eq, h_tick_eq, h_balance_eq]
129 -- Higher emotional weight means smaller discount factor
130 have h1 : 1 < φ := phi_gt_one
131 have h2 : 0 < φ := phi_pos
132 have h3 : 0 < 1 - 1/φ := by
133 have h4 : 1/φ < 1 := by rw [div_lt_one h2]; exact h1
134 linarith
135 -- discount1 < discount2 because emotional_weight1 > emotional_weight2
136 have h_discount_lt : 1 - trace1.emotional_weight * (1 - 1/φ) < 1 - trace2.emotional_weight * (1 - 1/φ) := by
137 have h_mul_lt : trace2.emotional_weight * (1 - 1/φ) < trace1.emotional_weight * (1 - 1/φ) :=
138 mul_lt_mul_of_pos_right h_more h3
139 linarith
140 -- Both discounts are positive
141 have h_disc1_pos : 0 < 1 - trace1.emotional_weight * (1 - 1/φ) := emotional_discount_pos trace1
142 have h_disc2_pos : 0 < 1 - trace2.emotional_weight * (1 - 1/φ) := emotional_discount_pos trace2
143 -- Base cost is positive (need at least one component positive)
144 have h_jcost_nonneg : 0 ≤ trace1.complexity * Jcost trace1.strength :=
145 mul_nonneg trace1.complexity_pos.le (Jcost_nonneg hs1)
146 have h_log_nonneg : 0 ≤ log (1 + (↑t - ↑trace1.encoding_tick) / ↑breath_cycle) := by
147 apply log_nonneg
148 have hd : 0 ≤ (↑t - ↑trace1.encoding_tick : ℝ) := by simp [sub_nonneg, Nat.cast_le, ht]
149 linarith [div_nonneg hd (le_of_lt breath_cycle_pos)]
150 have h_abs_nonneg : (0 : ℤ) ≤ |trace1.ledger_balance| := abs_nonneg _
151 have h_int_nonneg : 0 ≤ Jcost (1 + ↑|trace1.ledger_balance| / 10) := by
152 apply Jcost_nonneg
153 have h_cast_nonneg : (0 : ℝ) ≤ ↑|trace1.ledger_balance| := by norm_cast
154 linarith [div_nonneg h_cast_nonneg (by norm_num : (0 : ℝ) ≤ 10)]
155 -- Base cost is positive (at least one of the terms is strictly positive)
156 have h_base_pos : 0 < trace1.complexity * Jcost trace1.strength +
157 log (1 + (↑t - ↑trace1.encoding_tick) / ↑breath_cycle) +
158 Jcost (1 + ↑|trace1.ledger_balance| / 10) := by
159 rcases h_not_perfect with h_str | h_t | h_bal
160 · -- strength < 1 means Jcost > 0 (strength ≠ 1)
161 have h_ne_one : trace1.strength ≠ 1 := ne_of_lt h_str
162 have h_jcost_pos : 0 < Jcost trace1.strength := Jcost_pos_of_ne_one trace1.strength hs1 h_ne_one
163 have h_comp_pos : 0 < trace1.complexity * Jcost trace1.strength :=
164 mul_pos trace1.complexity_pos h_jcost_pos
165 linarith
166 · -- t > encoding_tick means log > 0
167 have h_log_pos : 0 < log (1 + (↑t - ↑trace1.encoding_tick) / ↑breath_cycle) := by
168 apply log_pos
169 have hd : 0 < (↑t - ↑trace1.encoding_tick : ℝ) := by
170 simp only [sub_pos, Nat.cast_lt]; exact h_t
171 linarith [div_pos hd breath_cycle_pos]
172 linarith
173 · -- ledger_balance ≠ 0 means interference cost > 0
174 have h_bal_pos : (0 : ℤ) < |trace1.ledger_balance| := abs_pos.mpr h_bal
175 have h_cast_pos : (0 : ℝ) < ↑|trace1.ledger_balance| := by exact_mod_cast h_bal_pos
176 have h_arg_pos : (0 : ℝ) < (1 : ℝ) + (↑|trace1.ledger_balance| : ℝ) / (10 : ℝ) := by
177 have hd : (0 : ℝ) < (↑|trace1.ledger_balance| : ℝ) / (10 : ℝ) := div_pos h_cast_pos (by norm_num)
178 linarith
179 have h_arg_ne_one : (1 : ℝ) + (↑|trace1.ledger_balance| : ℝ) / (10 : ℝ) ≠ (1 : ℝ) := by
180 have hd : (0 : ℝ) < (↑|trace1.ledger_balance| : ℝ) / (10 : ℝ) := div_pos h_cast_pos (by norm_num)
181 linarith
182 have h_int_pos : 0 < Jcost (1 + ↑|trace1.ledger_balance| / 10) :=
183 Jcost_pos_of_ne_one _ h_arg_pos h_arg_ne_one
184 linarith
185 -- Base cost for trace2 is the same (by h_base_eq), so also positive
186 have h_base2_pos : 0 < trace2.complexity * Jcost trace2.strength +
187 log (1 + (↑t - ↑trace2.encoding_tick) / ↑breath_cycle) +
188 Jcost (1 + ↑|trace2.ledger_balance| / 10) := by
189 rw [← h_base_eq]; exact h_base_pos
190 -- Final step: discount1 * base < discount2 * base (since discount1 < discount2 and base > 0)
191 -- We need to show: discount1 * base1 < discount2 * base2
192 -- Since base1 = base2 (by h_base_eq), we can rewrite and use mul_lt_mul_of_pos_right
193 calc (1 - trace1.emotional_weight * (1 - 1 / φ)) *
194 (trace1.complexity * Jcost trace1.strength +
195 log (1 + (↑t - ↑trace1.encoding_tick) / ↑breath_cycle) +
196 Jcost (1 + ↑|trace1.ledger_balance| / 10))
197 = (1 - trace1.emotional_weight * (1 - 1 / φ)) *
198 (trace2.complexity * Jcost trace2.strength +
199 log (1 + (↑t - ↑trace2.encoding_tick) / ↑breath_cycle) +
200 Jcost (1 + ↑|trace2.ledger_balance| / 10)) := by rw [h_base_eq]
201 _ < (1 - trace2.emotional_weight * (1 - 1 / φ)) *
202 (trace2.complexity * Jcost trace2.strength +
203 log (1 + (↑t - ↑trace2.encoding_tick) / ↑breath_cycle) +
204 Jcost (1 + ↑|trace2.ledger_balance| / 10)) :=
205 mul_lt_mul_of_pos_right h_discount_lt h_base2_pos
206
207/-! ## Forgetting Dynamics -/
208
209noncomputable def forgetting_rate (trace : LedgerMemoryTrace) (t : ℕ) : ℝ :=
210 base_decay_rate * memory_cost trace t / breath_cycle
211
212noncomputable def apply_forgetting (trace : LedgerMemoryTrace) (n_cycles : ℕ) (current_tick : ℕ) : ℝ :=
213 let rate := forgetting_rate trace current_tick
214 trace.strength * exp (-rate * n_cycles * working_memory_window)
215
216theorem forgetting_decreases (trace : LedgerMemoryTrace) (n m : ℕ) (t : ℕ)
217 (h : n ≤ m) (hs : trace.strength > 0) (ht : trace.encoding_tick ≤ t) :
218 apply_forgetting trace m t ≤ apply_forgetting trace n t := by
219 unfold apply_forgetting forgetting_rate
220 have h_mcost : 0 ≤ memory_cost trace t := memory_cost_nonneg trace t hs ht
221 have h_rate : 0 ≤ base_decay_rate * memory_cost trace t / breath_cycle :=
222 div_nonneg (mul_nonneg base_decay_rate_pos.le h_mcost) breath_cycle_pos.le
223 apply mul_le_mul_of_nonneg_left _ trace.strength_bounded.1
224 rw [exp_le_exp]
225 have h_nm : (n : ℝ) ≤ (m : ℝ) := by norm_cast
226 have h_window : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
227 nlinarith [mul_nonneg h_rate (le_of_lt h_window)]
228
229/-- Emotional memories forget slower -/
230theorem emotional_forgets_slower (trace1 trace2 : LedgerMemoryTrace) (n t : ℕ)
231 (h_same : trace1.complexity = trace2.complexity ∧
232 trace1.strength = trace2.strength ∧
233 trace1.encoding_tick = trace2.encoding_tick ∧
234 trace1.ledger_balance = trace2.ledger_balance)
235 (h_more : trace1.emotional_weight > trace2.emotional_weight)
236 (hs1 : trace1.strength > 0) (hs2 : trace2.strength > 0)
237 (ht1 : trace1.encoding_tick ≤ t) (ht2 : trace2.encoding_tick ≤ t)
238 (h_not_perfect : trace1.strength < 1 ∨ t > trace1.encoding_tick ∨ trace1.ledger_balance ≠ 0)
239 (hn : n > 0) :
240 apply_forgetting trace1 n t > apply_forgetting trace2 n t := by
241 unfold apply_forgetting forgetting_rate
242 -- trace1.strength = trace2.strength by h_same
243 have h_strength_eq : trace1.strength = trace2.strength := h_same.2.1
244 -- Lower cost => lower rate => smaller negative exponent => larger exp result
245 have h_cost_lt : memory_cost trace1 t < memory_cost trace2 t :=
246 emotional_reduces_cost trace1 trace2 t h_same h_more hs1 hs2 ht1 h_not_perfect
247 -- Rates: rate = base_decay_rate * cost / breath_cycle
248 have h_base_pos : 0 < base_decay_rate := base_decay_rate_pos
249 have h_breath_pos : 0 < (breath_cycle : ℝ) := breath_cycle_pos
250 have h_rate_lt : base_decay_rate * memory_cost trace1 t / breath_cycle <
251 base_decay_rate * memory_cost trace2 t / breath_cycle := by
252 apply div_lt_div_of_pos_right _ h_breath_pos
253 apply mul_lt_mul_of_pos_left h_cost_lt h_base_pos
254 -- Negative exponents: -rate1 * n * window > -rate2 * n * window (since rate1 < rate2)
255 have h_window_pos : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
256 have hn_pos : 0 < (n : ℝ) := by exact_mod_cast hn
257 have h_exp_arg_lt : -(base_decay_rate * memory_cost trace1 t / breath_cycle * n * working_memory_window) >
258 -(base_decay_rate * memory_cost trace2 t / breath_cycle * n * working_memory_window) := by
259 simp only [neg_lt_neg_iff]
260 apply mul_lt_mul_of_pos_right _ h_window_pos
261 apply mul_lt_mul_of_pos_right h_rate_lt hn_pos
262 -- exp is strictly increasing, so larger argument means larger result
263 have h_exp_lt : exp (-(base_decay_rate * memory_cost trace1 t / breath_cycle * n * working_memory_window)) >
264 exp (-(base_decay_rate * memory_cost trace2 t / breath_cycle * n * working_memory_window)) :=
265 exp_lt_exp.mpr h_exp_arg_lt
266 -- Finally, multiply by equal positive strengths
267 have hs_pos : 0 < trace1.strength := hs1
268 rw [h_strength_eq] at hs_pos
269 -- Need to show: str1 * exp(-rate1 * n * w) > str2 * exp(-rate2 * n * w)
270 -- Since str1 = str2 and exp(-rate1*n*w) > exp(-rate2*n*w)
271 have h_goal1 : trace1.strength * exp (-(base_decay_rate * memory_cost trace1 t / ↑breath_cycle) * ↑n * ↑working_memory_window)
272 = trace2.strength * exp (-(base_decay_rate * memory_cost trace1 t / ↑breath_cycle) * ↑n * ↑working_memory_window) := by
273 rw [h_strength_eq]
274 have h_goal2 : trace2.strength * exp (-(base_decay_rate * memory_cost trace1 t / ↑breath_cycle) * ↑n * ↑working_memory_window)
275 > trace2.strength * exp (-(base_decay_rate * memory_cost trace2 t / ↑breath_cycle) * ↑n * ↑working_memory_window) := by
276 apply mul_lt_mul_of_pos_left _ hs_pos
277 -- Both exponents are the same as h_exp_lt after simplification
278 have heq1 : -(base_decay_rate * memory_cost trace1 t / ↑breath_cycle) * ↑n * ↑working_memory_window
279 = -(base_decay_rate * memory_cost trace1 t / ↑breath_cycle * ↑n * ↑working_memory_window) := by ring
280 have heq2 : -(base_decay_rate * memory_cost trace2 t / ↑breath_cycle) * ↑n * ↑working_memory_window
281 = -(base_decay_rate * memory_cost trace2 t / ↑breath_cycle * ↑n * ↑working_memory_window) := by ring
282 rw [heq1, heq2]
283 exact h_exp_lt
284 linarith [h_goal1, h_goal2]
285
286/-! ## Thermodynamic Limits -/
287
288noncomputable def equilibrium_remember_prob (sys : RecognitionSystem) (trace : LedgerMemoryTrace) (t : ℕ) : ℝ :=
289 let J := memory_cost trace t
290 exp (-J / sys.TR) / (exp (-J / sys.TR) + 1)
291
292/-- At high temperature, p → 0.5 -/
293theorem high_temp_maximizes_entropy (trace : LedgerMemoryTrace) (t : ℕ) :
294 ∀ (ε : ℝ), ε > 0 → ∃ T₀ > 0, ∀ sys : RecognitionSystem, sys.TR > T₀ →
295 |equilibrium_remember_prob sys trace t - 0.5| < ε := by
296 intro ε hε
297 -- Let J = memory_cost trace t (some fixed real number)
298 set J := memory_cost trace t with hJ_def
299 -- Choose T₀ large enough that -J/T is small
300 -- We need |exp(-J/T) - 1| < 2ε to ensure |p - 0.5| < ε
301 -- Using the bound: |exp(x) - 1| ≤ |x| * exp(|x|) for small |x|
302 -- For T > |J|/(ε), we have |J/T| < ε, giving roughly |exp(-J/T) - 1| < ε*e^ε < 2ε
303 --
304 -- Simpler approach: use that |p - 0.5| = |e-1|/(2(e+1)) ≤ |e-1|/2
305 -- and |exp(x) - 1| → 0 as x → 0.
306 --
307 -- Take T₀ = max(1, |J|/ε + |J| + 1) to ensure |-J/T| < ε and well-behaved bounds
308 use max 1 ((|J| + 1) * (1/ε + 1))
309 constructor
310 · apply lt_max_of_lt_left; norm_num
311 · intro sys hT
312 have hT_pos : 0 < sys.TR := lt_of_lt_of_le (by norm_num : (0 : ℝ) < 1) (le_max_left _ _) |>.trans hT
313 unfold equilibrium_remember_prob; simp only
314 -- Let e = exp(-J/sys.TR)
315 set e := exp (-J / sys.TR) with he_def
316 have he_pos : 0 < e := exp_pos _
317 have h_denom_pos : 0 < e + 1 := by linarith
318 -- The key identity: p - 0.5 = (e - 1) / (2(e+1))
319 have h_05_eq : (0.5 : ℝ) = 1 / 2 := by norm_num
320 rw [h_05_eq]
321 have h_diff : e / (e + 1) - (1 : ℝ) / 2 = (e - 1) / (2 * (e + 1)) := by
322 field_simp
323 ring
324 rw [h_diff]
325 -- |p - 0.5| = |e - 1| / (2(e+1)) ≤ |e - 1| / 2 (since e+1 ≥ 1)
326 have h_abs_bound : |e - 1| / (2 * (e + 1)) ≤ |e - 1| / 2 := by
327 apply div_le_div_of_nonneg_left (abs_nonneg _)
328 · norm_num
329 · have h1 : 1 ≤ e + 1 := by linarith [he_pos]
330 linarith [mul_le_mul_of_nonneg_left h1 (by norm_num : (0 : ℝ) ≤ 2)]
331 rw [abs_div, abs_of_pos (by linarith : 0 < 2 * (e + 1))]
332 apply lt_of_le_of_lt h_abs_bound
333 -- Now we need |e - 1| / 2 < ε, i.e., |e - 1| < 2ε
334 -- Use Real.abs_exp_sub_one_le: if |x| ≤ 1, then |exp(x) - 1| ≤ 2 * |x|
335 have h_goal_equiv : |e - 1| / 2 < ε ↔ |e - 1| < 2 * ε := by
336 constructor
337 · intro h; have := (div_lt_iff₀ (by norm_num : (0 : ℝ) < 2)).mp h; linarith
338 · intro h; rw [div_lt_iff₀ (by norm_num : (0 : ℝ) < 2)]; linarith
339 rw [h_goal_equiv]
340 -- Need |e - 1| < 2 * ε
341 -- We have T > (|J|+1)*(1/ε+1), so |J|/T < ε when ε ≤ 1
342 -- For the exp bound, we need |-J/T| ≤ 1
343 have h_T_bound : sys.TR > (|J| + 1) * (1 / ε + 1) := lt_of_le_of_lt (le_max_right _ _) hT
344 have h_J_over_T : |J| / sys.TR < ε := by
345 have h1 : (|J| + 1) * (1 / ε + 1) > |J| / ε := by
346 have hε_pos : 0 < ε := hε
347 have h_pos : 0 < 1/ε + 1 := by linarith [one_div_pos.mpr hε_pos]
348 calc (|J| + 1) * (1 / ε + 1) = |J|/ε + |J| + 1/ε + 1 := by ring
349 _ > |J|/ε := by linarith [abs_nonneg J, one_div_pos.mpr hε_pos]
350 have h2 : sys.TR > |J| / ε := lt_trans h1 h_T_bound
351 have hT_pos' : 0 < sys.TR := hT_pos
352 rwa [div_lt_iff₀ hT_pos', mul_comm, ← div_lt_iff₀ hε]
353 -- Now check if |-J/T| ≤ 1 (needed for the exp bound)
354 have h_abs_small : |-J / sys.TR| ≤ 1 := by
355 have h_abs_TR : |sys.TR| = sys.TR := abs_of_pos hT_pos
356 rw [abs_div, abs_neg, h_abs_TR]
357 -- |J|/T ≤ 1 follows from T > |J| + 1
358 have h_one_le : 1 ≤ 1/ε + 1 := by linarith [one_div_pos.mpr hε]
359 have h1 : sys.TR > |J| + 1 := by
360 calc sys.TR > (|J| + 1) * (1/ε + 1) := h_T_bound
361 _ ≥ (|J| + 1) * 1 := mul_le_mul_of_nonneg_left h_one_le (by linarith [abs_nonneg J])
362 _ = |J| + 1 := mul_one _
363 have h2 : |J| / sys.TR < 1 := by
364 rw [div_lt_one (α := ℝ) hT_pos]
365 linarith
366 linarith
367 -- Apply the exponential bound
368 have h_exp_bound : |e - 1| ≤ 2 * |-J / sys.TR| := by
369 rw [he_def]
370 exact Real.abs_exp_sub_one_le h_abs_small
371 have h_abs_TR : |sys.TR| = sys.TR := abs_of_pos hT_pos
372 calc |e - 1| ≤ 2 * |-J / sys.TR| := h_exp_bound
373 _ = 2 * (|J| / sys.TR) := by rw [abs_div, abs_neg, h_abs_TR]
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
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 have h1 : J / (|log (ε / 2)| + 1) > 0 := div_pos hJ_pos h_denom_pos'
464 have h2 : sys.TR > 0 := hT_pos
465 -- -J/T < log ε ⟺ -log ε < J/T (after neg_lt)
466 rw [neg_div, neg_lt]
467 -- Now goal is: -log ε < J / sys.TR
468 -- Case split on whether ε ≥ 1
469 by_cases hε1 : 1 ≤ ε
470 · -- If ε ≥ 1, then log ε ≥ 0, so -log ε ≤ 0 < J/T
471 have h_log_nonneg : 0 ≤ log ε := log_nonneg hε1
472 have h_neg_log_le : -log ε ≤ 0 := neg_nonpos.mpr h_log_nonneg
473 have h_div_pos : 0 < J / sys.TR := div_pos hJ_pos h2
474 linarith
475 · -- If ε < 1, we have -log ε > 0, but J/T > |log(ε/2)| + 1 > |log ε|
476 push_neg at hε1
477 have h_log_neg : log ε < 0 := log_neg hε hε1
478 -- From hT_small: T < J / (|log(ε/2)| + 1), so J/T > |log(ε/2)| + 1
479 have h_J_div_T : J / sys.TR > |log (ε / 2)| + 1 := by
480 have h3 : sys.TR * (|log (ε / 2)| + 1) < J := by
481 calc sys.TR * (|log (ε / 2)| + 1) < (J / (|log (ε / 2)| + 1)) * (|log (ε / 2)| + 1) := by
482 apply mul_lt_mul_of_pos_right hT_small h_denom_pos'
483 _ = J := div_mul_cancel₀ J (ne_of_gt h_denom_pos')
484 -- (|log (ε / 2)| + 1) * sys.TR < J ⟺ |log (ε / 2)| + 1 < J / sys.TR
485 have h4 : (|log (ε / 2)| + 1) * sys.TR < J := by linarith [mul_comm sys.TR (|log (ε / 2)| + 1)]
486 exact (lt_div_iff₀ h2).mpr h4
487 -- Now show |log(ε/2)| ≥ |log ε|, i.e., -log(ε/2) ≥ -log ε
488 have h_half_pos : 0 < ε / 2 := by linarith
489 have h_half_lt_one : ε / 2 < 1 := by linarith
490 have h_log_half_neg : log (ε / 2) < 0 := log_neg h_half_pos h_half_lt_one
491 have h_half_lt_eps : ε / 2 < ε := by linarith
492 have h_log_mono : log (ε / 2) < log ε := log_lt_log h_half_pos h_half_lt_eps
493 -- |log(ε/2)| = -log(ε/2) > -log ε = |log ε|
494 have h_abs_compare : |log (ε / 2)| > |log ε| := by
495 rw [abs_of_neg h_log_half_neg, abs_of_neg h_log_neg]
496 linarith
497 -- -log ε = |log ε| < |log(ε/2)| < |log(ε/2)| + 1 < J/T
498 have h_neg_log : -log ε = |log ε| := by rw [abs_of_neg h_log_neg]
499 linarith
500 have h_exp_bound : e ≤ ε := by
501 rw [he_def]
502 have h1 : exp (-J / sys.TR) < exp (log ε) := exp_lt_exp.mpr h_arg_large
503 have h2 : exp (log ε) = ε := exp_log hε
504 linarith [h1, h2]
505 exact h_exp_bound
506
507/-! ## Learning and Consolidation -/
508
509structure LearningEvent where
510 experience : LedgerMemoryTrace
511 attention : ℝ
512 attention_bounded : 0 ≤ attention ∧ attention ≤ 1
513 repetitions : ℕ
514 spacing : ℕ
515
516noncomputable def spaced_bonus (event : LearningEvent) : ℝ :=
517 log (1 + event.spacing / working_memory_window) / log φ
518
519theorem spaced_bonus_nonneg (event : LearningEvent) : 0 ≤ spaced_bonus event := by
520 unfold spaced_bonus
521 apply div_nonneg
522 · apply log_nonneg
523 have hs : 0 ≤ (event.spacing : ℝ) := by norm_cast; omega
524 have hw : 0 < (working_memory_window : ℝ) := by norm_num [working_memory_window]
525 linarith [div_nonneg hs hw.le]
526 · exact log_nonneg Constants.phi_ge_one
527
528noncomputable def learning_rate (event : LearningEvent) : ℝ :=
529 φ ^ (-(event.repetitions : ℝ)) * event.attention * (1 + spaced_bonus event)
530
531theorem learning_rate_nonneg (event : LearningEvent) : 0 ≤ learning_rate event := by
532 unfold learning_rate
533 apply mul_nonneg
534 · apply mul_nonneg (rpow_pos_of_pos phi_pos _).le event.attention_bounded.1
535 · linarith [spaced_bonus_nonneg event]
536
537theorem learning_compounds (e1 e2 : LearningEvent)
538 (h_same : e1.experience = e2.experience)
539 (h_more : e1.repetitions > e2.repetitions)
540 (h_attn : e1.attention = e2.attention)
541 (h_space : e1.spacing = e2.spacing)
542 (hs1 : e1.experience.strength > 0) (_hs2 : e2.experience.strength > 0) :
543 let dr1 := -learning_rate e1 * memory_cost e1.experience e1.experience.encoding_tick
544 let dr2 := -learning_rate e2 * memory_cost e2.experience e2.experience.encoding_tick
545 dr1 ≥ dr2 := by
546 intro dr1 dr2
547 have h_pow_le : φ ^ (-(e1.repetitions : ℝ)) ≤ φ ^ (-(e2.repetitions : ℝ)) := by
548 apply rpow_le_rpow_of_exponent_le (le_of_lt phi_gt_one)
549 simp only [neg_le_neg_iff, Nat.cast_le]; exact Nat.le_of_lt h_more
550 have h_bonus : spaced_bonus e1 = spaced_bonus e2 := by unfold spaced_bonus; rw [h_space]
551 have h_lr_le : learning_rate e1 ≤ learning_rate e2 := by
552 unfold learning_rate; rw [h_attn, h_bonus]
553 apply mul_le_mul_of_nonneg_right _ (by linarith [spaced_bonus_nonneg e2])
554 apply mul_le_mul_of_nonneg_right h_pow_le e2.attention_bounded.1
555 have h_cost_same : memory_cost e1.experience e1.experience.encoding_tick =
556 memory_cost e2.experience e2.experience.encoding_tick := by rw [h_same]
557 have h_cost_nonneg : 0 ≤ memory_cost e1.experience e1.experience.encoding_tick :=
558 memory_cost_nonneg _ _ hs1 (le_refl _)
559 simp only [dr1, dr2]; rw [h_cost_same]; nlinarith
560
561def memory_ledger_status : List (String × String) :=
562 [ ("memory_cost_nonneg", "PROVEN")
563 , ("emotional_reduces_cost", "PROVEN")
564 , ("forgetting_decreases", "PROVEN")
565 , ("emotional_forgets_slower", "PROVEN")
566 , ("high_temp_maximizes_entropy", "PROVEN")
567 , ("low_temp_bistable", "PROVEN")
568 , ("learning_rate_nonneg", "PROVEN")
569 , ("learning_compounds", "PROVEN")
570 ]
571
572#eval memory_ledger_status
573
574end MemoryLedger
575end Thermodynamics
576end IndisputableMonolith
577