low_temp_bistable
plain-language theorem explainer
In the Recognition Science memory model any LedgerMemoryTrace satisfying the imperfection condition has strictly positive memory cost J. For such traces the equilibrium remember probability tends to zero as recognition temperature TR approaches zero. Researchers modeling retention as a thermodynamic process cite the result to establish low-temperature forgetting. The proof first derives J > 0 by case analysis on the three disjuncts using Jcost positivity lemmas, then constructs an explicit T0 that forces the Fermi-like probability below any ε.
Claim. Let trace be a LedgerMemoryTrace with strength > 0, encoding_tick ≤ t, and satisfying strength < 1 or t > encoding_tick or ledger_balance ≠ 0. Then for every ε > 0 there exists T₀ > 0 such that for any RecognitionSystem with TR < T₀ the equilibrium remember probability at time t satisfies p < ε (or p > 1 − ε).
background
The Memory Ledger module treats memory retention as a thermodynamic competition between free-energy decay and recognition cost. LedgerMemoryTrace is the structure carrying complexity (positive real), emotional_weight ∈ [0,1], encoding_tick, strength ∈ [0,1], ledger_balance, and consolidated flag. memory_cost combines an emotional discount factor, the base Jcost on strength, a logarithmic time-decay term, and an integer-balance correction. Upstream lemmas Jcost_nonneg and Jcost_pos_of_ne_one establish non-negativity and strict positivity of J(x) for x > 0, x ≠ 1 via the squared representation J(x) = (x−1)²/(2x).
proof idea
The tactic proof first sets J := memory_cost trace t and proves 0 < J by case split on h_not_perfect. The strength < 1 case invokes Jcost_pos_of_ne_one; the t > encoding_tick case uses log_pos on the time term; the nonzero-balance case applies Jcost_pos_of_ne_one to the shifted argument. With J positive it selects T₀ = min(1, J / (|log(ε/2)| + 1)). For TR < T₀ it shows e = exp(−J/TR) satisfies e/(e+1) < ε by proving the inequality e/(e+1) < e and bounding the exponential via the chosen T₀.
why it matters
The result is referenced by the memory_ledger_status definition that records the module’s complete proof list. It supplies the low-temperature limit for imperfect traces inside the thermodynamic memory treatment, confirming that J > 0 drives retention probability to zero. Within the Recognition Science framework it closes one of the final claims in the Memory Ledger module, consistent with J-cost positivity from the forcing chain and the overall absence of sorries in the thermodynamics section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.