Model catalog
Economoist ships a catalog of economic models with structural properties proven by cvc5 over the reals. Each property listed below carries an unqualified SMT green at the stated dimension.
Markov chains
Section titled “Markov chains”The finite-state Markov transition operator, represented as a row-stochastic matrix.
Proven properties:
- Simplex preservation under one step. If the input distribution lies on the probability simplex (non-negative entries summing to one), the output after one matrix-vector multiply remains on the simplex.
- Structural greens at n=2 and n=3. The simplex-preservation property is discharged for concrete 2-state and 3-state chains. These are fixed-dimension instances, not the general-n theorem.
Bellman operator
Section titled “Bellman operator”The standard dynamic-programming Bellman operator mapping a value function to its one-step update.
Proven properties:
- Monotonicity. If value function f is pointwise less than or equal to g, then the Bellman image of f is pointwise less than or equal to the Bellman image of g.
- Boundedness. If the input value function is bounded within an interval, the output remains within a computable interval determined by the reward bounds and discount factor.
- Single-application contraction. One application of the operator reduces the sup-norm distance between any two bounded value functions by the discount factor. This is the single-step inequality, not the fixed-point convergence theorem.
- Structural greens at n=2 and n=3. Monotonicity, boundedness, and single-application contraction are discharged for 2-state and 3-state instances.
Growth and present value
Section titled “Growth and present value”Scalar growth models and present-value identities.
Proven properties:
- Gordon model positivity. When the discount rate strictly exceeds the growth rate and both are positive, the Gordon present-value formula yields a strictly positive value.
- Gordon model monotonicity. The present value is strictly increasing in the dividend and strictly decreasing in the discount rate (holding growth fixed).
- AD comparative statics with proven signs. Automatic differentiation of the Gordon formula produces partial derivatives whose signs are discharged by the solver: positive with respect to dividend and growth, negative with respect to discount.
- Dimension-free (scalar). These properties involve no matrices. They are univariate or bivariate real-arithmetic statements and are proven without fixing a state-space dimension.