Economoist model guide
Economoist checks specific claims about three models. Each page names the assumptions, the result checked, and what lies outside that result.
Models
Section titled “Models”- Markov chains: one transition at two and three states, distribution-type obligations, exact mass preservation, and nonnegative output masses under their respective guards.
- Bellman operator: one update at two and three states with two actions, state-0 monotonicity and boundedness, plus a two-sided contraction bound at each output state.
- Gordon present value: positivity and two-point comparisons for
D / (r - g), a stricter discount-spread variant, and a separate sampled AD check.
Reading proof results
Section titled “Reading proof results”The SMT-checked goals establish their stated claims over the reals under the written assumptions. They do not establish floating-point behavior, iteration limits, or results at dimensions absent from the model.
The Gordon sensitivity example uses sampling to check an automatic-differentiation result at selected inputs. Sampling is numerical evidence, not a proof over the full domain. Concrete example programs are available in the Economoist repository.