Page actions
instrument mechanism / verified-with-binding-errata
Markov Chain Simulator mechanism
The inspectable method record for Markov Chain Simulator, kept separate from implementation and qualification.
Model scope
The core algorithms are correct for finite discrete-time Markov chains using row distributions: solve πP=π with sum(π)=1, and compute μP^n. Verdict is NEEDS_REVIEW because the spec does not explicitly define row versus column orientation or whether "initial state" means a one-hot state or an already supplied distribution. The honest-label assumptions about irreducibility and aperiodicity are appropriate but should explicitly distinguish uniqueness of stationarity from convergence.
- The formulas are mathematically standard under a row-vector convention: a stationary distribution satisfies πP=π, and an initial row distribution μ evolves as μP^n.
- The input is described as an "initial state" rather than an initial distribution. If a single state is supplied, the implementation must convert it to the corresponding one-hot row vector before applying μP^n.
- The matrix orientation is not explicitly stated. With column-vector distributions, the equivalent evolution is P^nμ and the stationary equation is Pπ=π; the current formulas require row vectors.
- A finite stochastic chain always has at least one stationary distribution, but uniqueness requires irreducibility, and convergence of μP^n to it requires aperiodicity in addition to irreducibility.
- The implementation must validate that P is square, every entry is nonnegative, and every row sums to 1 under the stated row-vector convention.
Units and conventions
- Transition probabilities and state-distribution entries are dimensionless values in [0,1].
- Each row of P must sum to exactly 1, subject only to a documented numerical tolerance.
- n is a nonnegative integer; n=0 means P^0=I and the distribution remains the initial distribution.
Inspectable vector
One of 4 source-bound review vectors:
{
"inputs": {
"transition_matrix": [
[
0.8,
0.2
],
[
0.3,
0.7
]
],
"initial_state_distribution": [
1,
0
],
"n": 3
},
"expected_outputs": {
"steady_state": [
{
"exact": "3/5"
},
{
"exact": "2/5"
}
],
"state_distribution_at_n": [
{
"exact": "13/20"
},
{
"exact": "7/20"
}
]
},
"reference_data": {
"chain_type": "irreducible and aperiodic",
"row_convention": "mu_next=mu P"
},
"working": "Let π=[a,b]. From πP=π: a=0.8a+0.3b, so 0.2a=0.3b and a:b=3:2. Therefore π=[3/5,2/5]. Compute P^2=[[0.8*0.8+0.2*0.3, 0.8*0.2+0.2*0.7],[0.3*0.8+0.7*0.3, 0.3*0.2+0.7*0.7]]=[[0.70,0.30],[0.45,0.55]]. Then P^3 first row is [0.70*0.8+0.30*0.3, 0.70*0.2+0.30*0.7]=[0.65,0.35]=[13/20,7/20]. Since the initial distribution is [1,0], [1,0]P^3 is the first row of P^3."
}Failure boundary
BREAK_CLAIMED · SELF_FLAGGED
The undefined-result vector exposes a singular stationary solve that must be rejected or reported as non-unique. The convention probe also shows that an unspecified row-versus-column convention can produce an invalid distribution summing to 1.1 if the displayed matrix is used with the wrong multiplication orientation.
Other records
Sources and evidence
These pointers bind the page to evidence. They do not grant authority or collapse verification into deployment.
VERIFIED_LEDGER.jsonevidence-tranche8/tranche8-results.jsonBOUNDARY_HAZARD_CATALOG.json