Harvestability
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
We study a narrow horizon-dependent allocation question in a CRRA investor setting with Ornstein-Uhlenbeck eigenmodes. The paper centers the fin_harvestability function
\[
h(T,\tau)=1-e^{-T/\tau},
\]
interpreted as the closed-form horizon-dependent correction term around the myopic Merton benchmark.
Length
2,444 words
Status
Draft