# Success and failure after four steps

KL-FCS-058 · Finite probability · version 1.0.0

## Problem

Compute the exact distribution at each step of a finite Markov chain.

## Context

Propagate a probability distribution through an explicitly finite stochastic model with exact fractions.

## Definitions

- **DTMC**: A discrete-time Markov chain whose row probabilities determine the next-state distribution.
- **Stochastic matrix**: A nonnegative matrix with every row summing to one.
- **Absorbing state**: A state that transitions to itself with probability one.

## Checked result

Final probability distribution: ["1/16", "15/32", "15/32"].

Each step distributes the current mass across outgoing transitions. Absorbing rows retain their mass, and every row of the artifact preserves total probability one.

## Checker reasoning

1. Validate the initial distribution and each matrix row.
2. Multiply the row distribution by the transition matrix.
3. Repeat for the exact declared horizon.
4. Compare every trajectory row and the final rational distribution.

## Dataset construction

{
  "family": "probability",
  "task": "Compute the exact distribution at each step of a finite Markov chain.",
  "input_encoding": "Structured JSON; field meanings are stated in the specification.",
  "coverage": "Exact rational trajectory · 4 transitions",
  "acceptance": [
    "Validate the initial distribution and each matrix row.",
    "Multiply the row distribution by the transition matrix.",
    "Repeat for the exact declared horizon.",
    "Compare every trajectory row and the final rational distribution."
  ],
  "generation": "Deterministic finite fixture; full enumeration or witness replay as stated.",
  "split_policy": "Reference corpus for exposition and reproduction; no train/test evaluation split is claimed."
}

## Formal payload

```json
{
  "specification": {
    "transition": [
      [
        "1/2",
        "1/4",
        "1/4"
      ],
      [
        "0",
        "1",
        "0"
      ],
      [
        "0",
        "0",
        "1"
      ]
    ],
    "initial": [
      "1",
      "0",
      "0"
    ],
    "steps": 4,
    "semantics": "Discrete time, row-stochastic transition matrix, no nondeterministic scheduler."
  },
  "claim": {
    "distribution": [
      "1/16",
      "15/32",
      "15/32"
    ]
  },
  "witness": {
    "trajectory": [
      [
        "1",
        "0",
        "0"
      ],
      [
        "1/2",
        "1/4",
        "1/4"
      ],
      [
        "1/4",
        "3/8",
        "3/8"
      ],
      [
        "1/8",
        "7/16",
        "7/16"
      ],
      [
        "1/16",
        "15/32",
        "15/32"
      ]
    ]
  }
}
```

## Complexity

A dense n-state chain over h steps costs O(hn²) arithmetic operations, with fraction sizes growing over time.

## Limits

The result is for the declared horizon. The browser chart uses floating-point display; Python fractions establish the exact certificate.

## Common error and further work

A finite-horizon probability is not automatically an eventual-reachability answer.

Add absorbing-state equations, expected hitting time, and nondeterministic MDP choices.

## Verification

Exact rational trajectory · 4 transitions. 4 checker units.
Replay with `python3 tools/verify.py`. Mechanical status: checked; human review
has not yet been recorded. Custom Python verification, not a proof-assistant
claim. Checker 1.0.0 and exact source hashes are in `verification.json`.

## Provenance and references

Original Kenton Labs reference instance, authored with Codex assistance on 2026-10-11.
No external dataset or model-generation experiment. Reuse-license selection
remains pending.

- [Conceptual reference](https://www.prismmodelchecker.org/doc/whatsinprism.php)