Boundaries
One step and repeated updates
Section titled “One step and repeated updates”The Bellman checks cover one application of an operator. They do not check
that repeated applications converge to a fixed point. The Gordon checks
establish properties of d / (r - g) under stated guards; they do not
establish convergence of a cash-flow series.
Fixed dimensions
Section titled “Fixed dimensions”The checked Markov and Bellman instances have two or three states. Their results do not establish the same statements for every state-space size. The Bellman instances have two actions per state. The Gordon expression has no state dimension.
Reals and floating point
Section titled “Reals and floating point”cvc5 checks the listed properties using mathematical real arithmetic. A
result over reals does not establish identical f32 or f64 execution
after rounding. The sampled automatic-differentiation check uses f32
execution but does not establish a result for every input.
Read each result
Section titled “Read each result”Each result applies only under its stated assumptions. The model guide summarizes the checked claims and their limits.