minimumErasurePower
plain-language theorem explainer
Minimum power to erase one bit once per recognition tick equals Landauer energy at temperature T divided by the fundamental timescale τ₀ (in seconds). Information theorists and RS thermodynamicists cite it when turning the static Landauer energy floor into a continuous power bound set by the recognition clock. The body is the direct quotient of the already-defined Landauer energy by τ₀.
Claim. For temperature $T\in\mathbb{R}$, the minimum power for one-bit erasure per recognition tick is $E_{\mathrm{L}}(T)/\tau_0$, where $E_{\mathrm{L}}(T)$ is the Landauer energy $k_B T\ln 2$ and $\tau_0$ is the fundamental recognition timescale in seconds.
background
Module INFO-004 derives Landauer's bound from Recognition Science's fundamental timescale $\tau_0$. Classically, erasing one bit dissipates at least $E_{\min}=k_B T\ln 2$ as heat: one bit of uncertainty is removed, entropy rises by $k_B\ln 2$, and the heat cost is $T\Delta S$.
In RS the same floor is read as a recognition cost paid on the $\tau_0$ clock. Erasure is "recognize the current state, then reset"; that process carries a J-cost, and $\tau_0$ sets the rate at which the thermodynamic minimum can be paid. Sibling definitions supply Boltzmann's constant, room temperature, the Landauer energy $E_{\mathrm{L}}(T)$, and $\tau_0$ in seconds.
Upstream cost constructions (observer J-cost on recognition events, multiplicative-recognizer derived cost, rung-coarsen total cost) fix the meaning of "cost" as non-negative J-type recognition cost; this definition only converts the energy scale into power via $\tau_0$.
proof idea
Pure definitional quotient: return landauerEnergy T divided by tau0_seconds. No lemmas, no tactics, no positivity or units proof at this site; those live on the sibling energy and timescale declarations.
why it matters
Closes the power half of INFO-004: once Landauer energy is available from $k_B T\ln 2$, dividing by $\tau_0$ yields the minimum continuous power for one erasure per recognition tick. That rate link is what lets RS treat Landauer as a consequence of the recognition clock rather than an external thermodynamic postulate.
The next section in the same module ("The J-Cost Connection") introduces erasure J-cost and the claim that it matches the thermodynamic Landauer value; this power definition sits immediately upstream of that comparison. No downstream theorems currently consume it (used_by empty), so it is infrastructure for the planned thermodynamics-of-information paper and for ultra-low-power computing bounds approaching the Landauer limit. Framework landmarks: $\tau_0$ as the fundamental tick, J-cost as recognition cost, and the eight-tick octave only indirectly via the shared timescale.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.