emotional_discount_pos
plain-language theorem explainer
The lemma shows that for any memory trace the factor 1 minus emotional weight times (1 minus one over phi) is strictly positive. Thermodynamic models of retention in Recognition Science cite it to guarantee nonnegative contributions to free-energy expressions. The tactic proof chains bounds on phi greater than one with the interval constraint on emotional weight and finishes with linarith after invoking one_mul.
Claim. Let $w$ be the emotional weight of a memory trace satisfying $0 ≤ w ≤ 1$. Then $0 < 1 - w(1 - φ^{-1})$, where $φ$ denotes the golden-ratio fixed point.
background
LedgerMemoryTrace is the structure that records a single memory event: it carries a complexity value, an emotional_weight in the closed unit interval, a strength, an encoding tick, and a consolidated flag. The module treats memory retention as a thermodynamic process in which free-energy decay competes with recognition cost, using the Recognition Composition Law to relate J-cost terms across scales. The upstream result one_mul supplies the algebraic identity needed to simplify the product bound inside the proof.
proof idea
The tactic sequence first records phi_gt_one and phi_pos, derives 0 < 1/φ and 1/φ < 1, then obtains 0 < 1 - 1/φ by linarith. It pulls the boundedness hypothesis emotional_bounded from the trace, applies mul_le_mul_of_nonneg_right to cap the product at 1 - 1/φ, rewrites the right-hand side via one_mul, and concludes with a final linarith step.
why it matters
The positivity result is invoked directly by memory_cost_nonneg to factor the cost expression and by emotional_reduces_cost to compare traces differing only in emotional weight. It therefore anchors the claim that emotional weighting lowers effective memory cost inside the low-temperature bistable regime. The lemma closes one link in the thermodynamic memory chain that begins from the phi-ladder and the eight-tick octave of the forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.