The mathematics of your money.

Act 1 · prospect theory

What is risk?

The textbook answer is the standard deviation of returns. That is correct. It is also useless to anyone who has ever watched a $1,000 loss and a $1,000 gain feel like different species of event.

Kahneman and Tversky proposed a value function v(x) that bends sharply at zero: concave above, convex below, and steeper on the loss side. Calibrated to humans, the loss-aversion coefficient is roughly λ ≈ 2.25. A loss feels 2.25× as bad as the equivalent gain feels good.

That number is not a metaphor. The Lean theorem Becky.Psychology.ProspectTheory.loss_aversion formalizes the asymmetry: whenever the curvature exponents agree (α = β), |v(−x)| > v(x). Kernel-checked.

Act 2 · the game against yourself

The Kelly fraction

If you keep playing the same favourable bet over and over — which is what staying invested actually is — there is exactly one bet size that maximises the long-run growth rate of your wealth. It is called the Kelly fraction:

f* = (μ − r_f) / σ²

For a 10% expected market return, a 6.49% mortgage rate as the risk-free benchmark, and a 15% volatility, full Kelly says invest 156% of your slack — i.e. lever up.

That is the math. The math is correct. The Lean theorem Becky.Finance.KellyCriterion.kelly_maximizes_log_growth proves f* is the unique zero of the log-growth derivative. The practical recommendation, even from Kelly himself, is half-Kelly: you give up about 25% of the growth rate in exchange for far less ruin risk. Over-Kelly is more dangerous than under-Kelly.

Act 3 · the market is not a coin flip

Fat tails and volatility drag

Stock prices follow a geometric Brownian motion to a first approximation. The Itô-corrected drift is μ − σ²/2: the median investor gets the arithmetic mean MINUS half the variance. That subtracted term is the volatility drag, and it is Jensen’s inequality wearing a suit.

At σ = 15% the drag is 1.125% a year. At σ = 25% it is 3.125%. At σ = 40% — the crash regime in this corpus — it is 8%. The difference between “the market averages 10%” and what your portfolio actually does is exactly this term.

Real markets are also not single-regime. The fan to your left is a regime-switching Markov model with three states (bull / bear / crash) and a stationary distribution of roughly 70/22/8. It produces fat tails — the kind that make a 1-in-100 year happen every twenty years.

Act 4 · the macro context

Why 6.49%?

A 6.49% 30-year mortgage rate is not a number; it is a story. The Federal Reserve sets a target for the overnight rate. The Treasury market sets the 10-year yield as a long-run forecast of that target plus a term premium. Your mortgage is roughly the 10-year yield plus a credit spread of 150–250 basis points.

For Becky’s case the relevant comparison is not 6.49% vs the S&P. It is 6.49% on the mortgage versus the after-tax, after-drag, regime-switching expected return on the brokerage account. Once you carry every term, the gap narrows from “obvious” to “a real decision.”

A 6.49% guaranteed return is mathematically very competitive. It is also psychologically very competitive — the prospect theory in Act 1 says paying down debt feels like a gain twice, once for the principal reduction and once for not losing it in a crash. The math and the gut, for once, agree.

Act 5 · the synthesis

The honest answer

Three strategies. All to mortgage. All to market. Fifty-fifty split. The bars to your left are the deterministic terminal wealth at 30 years; the whiskers are the worst-to-best span from a Monte Carlo run.

On expected value, the market wins. On regret minimisation, the mortgage wins. On the worst 5% of paths, the split wins. There is no single “correct” answer because there is no single question — what you are really choosing is which loss function you can live with.

The kernel can prove the Kelly fraction is f*. The kernel can prove the loss-aversion asymmetry. The kernel cannot prove which of those two facts matters more to you at 3 a.m. when the S&P is down 28%. That part is yours.

For Becky. Built on the Lean 4 corpus at ~/becky. 162 theorems, 0 sorry, kernel-clean. The math is the gift; the decision is yours.