high_temp_maximizes_entropy
plain-language theorem explainer
High temperature forces the equilibrium retention probability of any fixed memory trace to approach one half. Researchers modeling memory as a thermodynamic system governed by J-cost would cite this to establish the high-T entropy maximum. The proof constructs an explicit T0 from the memory cost J and ε, then applies the bound |exp(x)-1| ≤ 2|x| for |x|≤1 together with algebraic rearrangement of p = e/(e+1) to control the deviation.
Claim. Let $J$ be the memory cost of a trace at fixed time $t$. For every $ε>0$ there exists $T_0>0$ such that for every recognition system with temperature $T_R>T_0$, the equilibrium retention probability $p$ satisfies $|p-1/2|<ε$.
background
Memory is represented by the LedgerMemoryTrace structure, which packages an identifier, positive complexity, emotional weight in [0,1], encoding tick, strength in [0,1], and a consolidation flag. The module treats retention as a thermodynamic competition between this cost and free-energy decay, with equilibrium probability derived from the Boltzmann factor exp(-J/T_R).
proof idea
The tactic proof fixes ε>0, sets J := memory_cost trace t, and chooses T0 = max(1,(|J|+1)(1/ε+1)). For T_R > T0 it defines e = exp(-J/T_R), rewrites the deviation as |e-1|/(2(e+1)), bounds the denominator factor by 1/2, and invokes Real.abs_exp_sub_one_le once |J/T_R|≤1 is verified by the choice of T0. Arithmetic lemmas lt_trans and mul_one close the final inequalities.
why it matters
The theorem supplies the high-temperature limit required for the complete list of proven memory theorems in memory_ledger_status. It realizes the entropy-maximization consequence of the Recognition Composition Law at the level of memory traces, consistent with the J-uniqueness and phi-ladder structure of the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.