Boundaries

Economoist's SMT greens are genuine proofs, but they cover a specific region of the mathematical landscape. Three boundaries define what sits outside that region.

Limit and fixed-point results

Convergence theorems (e.g., the Bellman operator converges to a unique fixed point under repeated application) require induction over an unbounded number of iterations. The SMT tier works over quantifier-free or existentially quantified formulas in a single step. Inductive arguments are out of scope. Economoist proves the single-step contraction inequality; the limit theorem built from it is not claimed.

Fixed dimension

Structural greens are discharged at small, fixed dimensions: n=2 and n=3 for Markov chains and Bellman operators. These are concrete instances, not the general-n statement. The general theorem ("for all n, the property holds") requires universally quantified reasoning over matrix dimension, which the SMT encoding does not attempt.

Reals vs floats

All proofs are carried out over the mathematical reals (the Real sort in SMT-LIB). They say nothing about f32 or f64 floating-point behavior. Rounding, overflow, subnormal arithmetic, and catastrophic cancellation are not modeled. If you need guarantees about IEEE 754 execution, those require a separate floating-point verification layer.