Gordon present value

The Gordon present-value model is

[ P = \frac{D}{r-g} ]

where D is the next-period dividend, r is the required return, and g is the dividend growth rate. For the usual economic interpretation, use D > 0 and 0 <= g < r < 1. The denominator must be positive, and the discounted-dividend series converges under these rate assumptions.

Functions and rate checks

gordon_pv(d, r, g) evaluates the closed form. Use a checked function when rates come from data:

• gordon_pv_checked(d, r, g) returns Some(value) when r > g, otherwise None.
• gordon_pv_strict_checked(d, r, g) returns Some(value) when r > g + 0.01, otherwise None.

These checks apply only to the rate inequality they name. They do not verify that d is positive, that the result is finite, or that rates are in the usual economic range. A Some value is therefore not by itself a guarantee of a positive or economically meaningful valuation.

The stricter function uses the same formula with a wider rate spread. It is a choice for callers who want additional separation between return and growth, not a different valuation model.

What has been checked

SMT-checked properties cover positivity and selected two-point comparisons under their stated assumptions. They reason about the formula over the reals; they do not establish floating-point behavior for every input. A separate sampled example checks the sign of the automatic-differentiation sensitivity to r at selected inputs. Sampling is numerical evidence, not a proof over the full domain.

See the model guide for the Markov and Bellman models and the limits of their checked claims.