Markov transitions

Economoist.Markov defines one transition of a distribution across two or three states. For input masses p and transition matrix T, each output mass is the sum of the input masses weighted by the corresponding column of T. The package provides separate Dist2 and Dist3 types and advance functions for the two sizes.

Checked properties

The goals in properties/markov.ch call the exported next_mass or mass3_next functions. Chelis checks each goal over real arithmetic.

Goal	Guards	Result for one transition
markov_mass_preserved, markov3_mass_preserved	Input masses sum exactly to one; every transition row sums exactly to one	Output masses sum exactly to one
markov_nonneg_preserved, markov3_nonneg_preserved	Input masses and transition entries are nonnegative	Every output mass is nonnegative

Mass preservation and nonnegativity are separate claims with separate assumptions; neither follows from the other.

Dist2 and Dist3 have a different, guarded contract: their masses are nonnegative and their sum lies within 0.0001 of one. The constructor and advance producer obligations check that returned distributions satisfy this invariant. The type invariant allows a mass tolerance, whereas the separate mass-preservation goals above assume and prove exact sums.

What advance admits

advance and advance3 admit a transition when all three of these hold, and return None otherwise:

1. every transition entry is nonnegative;
2. every row sum lies within 0.0001 of one, using the distribution invariant's eps() band;
3. the masses the step computes sum to within 0.0001 of one.

Condition 2 is a tolerance on representation, not an allowance on row-stochasticity. A row whose own sum is more than 0.0001 from one is refused, and so is a row sitting exactly at that distance, because the f32 sum of its entries falls an ulp outside the f32 band endpoint. A transition matrix estimated from data may therefore still need normalizing before advance will admit it.

The step checks the masses it actually computes, not just the input matrix. This prevents rounding error from carrying a result outside the distribution's tolerance band. Output nonnegativity is not part of this run-time check, and real-arithmetic properties do not establish every f32 result.

markov_mass_preserved assumes exact row sums. It does not cover rows admitted only by the tolerance in condition 2; those rows depend on the runtime output check in condition 3. Repeated calls to advance can accumulate drift until that check fails and the function returns None. Admission therefore depends on the distribution produced by earlier calls as well as the transition matrix.

Scope

These checks cover one transition at two states and one at three states. They do not establish a result for arbitrary state counts. They also do not prove the existence or uniqueness of a stationary distribution, convergence of repeated transitions, or ergodicity.

The source uses f32 values, but an SMT result concerns the corresponding real-arithmetic expression. It does not guarantee that every floating-point run preserves an exact sum. The constructors and transition functions check the tolerance band at run time and return Option when an input or result falls outside it.