breath_cycle_pos
plain-language theorem explainer
Establishes that the breath cycle constant equals 1024 and is strictly positive over the reals. Memory thermodynamics researchers cite it when bounding decay rates of the form base_decay_rate times memory_cost divided by breath_cycle. The argument is a direct term-mode reduction that unfolds the constant definition and invokes norm_num.
Claim. The breath cycle period $B$ satisfies $0 < B$ in the reals, where $B := 1024$.
background
The MemoryLedger module treats memory as a thermodynamic system in which retention competes with free-energy decay under Recognition Science rules. breath_cycle supplies the fixed natural number 1024 that appears in decay-rate expressions such as base_decay_rate * memory_cost / breath_cycle. Cost is the abbreviation Quantity CostUnit drawn from RSNative.Core and used to measure nonnegative J-costs of memory traces.
proof idea
Unfolds the definition of breath_cycle to expose the literal 1024, then applies norm_num to discharge the inequality 0 < 1024. No external lemmas are invoked; the proof is a pure computational check.
why it matters
Supplies the positivity needed by five downstream theorems: emotional_forgets_slower, emotional_reduces_cost, forgetting_decreases, low_temp_bistable, and memory_cost_nonneg. These results establish monotonicity of forgetting, emotional cost reduction, and low-temperature bistability. It closes a required positivity gap inside the fully-proven thermodynamic memory chain and aligns with the eight-tick octave scaling of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.