Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 4 results · all verified · 4 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 4 also cleared it.

Finite Trellises, Viterbi, and Sequence Decoding — Examples

1 · Prerequisites

Finite Trellises, Viterbi, and Sequence Decoding

2 · Summary

Worked finite models show how ties and unreachable trellis states affect traceback, how exact HMM path masses determine a sequence MAP, and why zero observation evidence leaves no posterior MAP path. A second HMM calculation distinguishes a whole-sequence MAP from independently maximizing each time-indexed posterior marginal.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Zero-evidence observations have no conditional MAP path

Statement refuted

For every finite HMM and every finite observation sequence, the posterior distribution on hidden paths is defined and therefore has a sequence MAP path.

Facts & Assumptions

Given: A finite discrete HMM with two hidden states and one observed symbol.

[F1]

Finite hidden Markov models for sequence decoding: For an observation sequence $y$ , its evidence is $p (y) = \sum_{z} p (z, y)$ ; the conditional path mass $p (z ∣ y) = p (z, y) / p (y)$ is defined only when $p (y) > 0$ , and a sequence MAP path maximizes this conditional mass.

Counterexample

Take $S = {u, v}$ , $Y = {0, 1}$ , and initial probabilities $π (u) = π (v) = 1 / 2$ . Let both transition rows be $(1 / 2, 1 / 2)$ . In each state let $B (s, 0) = 1$ and $B (s, 1) = 0$ . These are normalized initial, transition, and emission parameters. Observe the length-one sequence $y = (1)$ .

1.1givenF1algebra

For the two possible hidden paths, the joint masses are $p ((u), (1)) = (1 / 2) \cdot 0 = 0$ and $p ((v), (1)) = (1 / 2) \cdot 0 = 0$ . Thus $p ((1)) = 0 + 0 = 0$ .

2.1givenF1step 1.1algebra∎

By [F1], division by this zero evidence does not define conditional path masses, so there is no posterior MAP path for this observation. Both paths maximize the zero joint mass, but that arbitrary tie is not a conditional posterior distribution. This refutes the Statement.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

Coordinatewise posterior modes need not be a sequence MAP

Statement refuted

For every finite HMM with positive observation evidence, choosing a posterior-most-probable hidden state separately at each time always produces a sequence MAP path.

Facts & Assumptions

Given: A finite discrete HMM, an observation sequence $y$ , and $p (y) > 0$ . The time- $t$ posterior marginal at state $s$ is $\sum_{z : z_{t} = s} p (z ∣ y)$ .

[F1]

Finite hidden Markov models for sequence decoding: For positive evidence, $p (z ∣ y) = p (z, y) / p (y)$ ; a sequence MAP path maximizes this whole-path conditional mass.

Counterexample

Let $S = {u, v}$ and $Y = {x}$ . Set $π (u) = 7 / 20$ and $π (v) = 13 / 20$ . The transition rows are $u \to (u, v) = (1, 0)$ and $v \to (u, v) = (34 / 65, 31 / 65)$ . Both states emit $x$ with probability $1$ . Observe $y = (x, x)$ . The four hidden-path masses are $p (u u, y) = 7 / 20, p (u v, y) = 0, p (v u, y) = 17 / 50, p (v v, y) = 31 / 100.$ They sum to $1$ , so these are also the posterior path masses.

1.1givenF1algebra

The initial weights sum to $1$ , each transition row sums to $1$ , and each emission row has its single entry equal to $1$ , so this is a valid HMM. The path masses follow by multiplying the initial and transition factors: $u u = (7 / 20) \cdot 1 = 7 / 20$ , $u v = (7 / 20) \cdot 0 = 0$ , $v u = (13 / 20) (34 / 65) = 17 / 50$ , and $v v = (13 / 20) (31 / 65) = 31 / 100$ . Their sum is $35 / 100 + 0 + 34 / 100 + 31 / 100 = 1$ .

2.1givenF1step 1.1algebra∎

The time-1 marginal masses are $P (Z_{1} = u ∣ y) = 35 / 100$ and $P (Z_{1} = v ∣ y) = 65 / 100$ , so the unique time-1 mode is $v$ . The time-2 marginal masses are $P (Z_{2} = u ∣ y) = 35 / 100 + 34 / 100 = 69 / 100$ and $P (Z_{2} = v ∣ y) = 31 / 100$ , so the unique time-2 mode is $u$ . Their coordinatewise mode is $v u$ , whose mass $17 / 50 = 34 / 100$ is strictly below $p (u u ∣ y) = 7 / 20 = 35 / 100$ . Hence $v u$ is not a sequence MAP path, refuting the Statement.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

A finite trellis with tied maxima and an unreachable high-score state

Example

Take $T = 3$ , vertex layers $V_{1} = {s}$ , $V_{2} = {a, b, c}$ , and $V_{3} = {t}$ . Set $α (s) = 1$ and $β (t) = 1$ . The only layer-2 edges are $s \to a$ and $s \to b$ , each of weight $2$ . The layer-3 edges are $a \to t$ and $b \to t$ , each of weight $3$ , and $c \to t$ of weight $100$ . The vertex order in layer 2 is $a < b < c$ .

Columns in the diagram are layers and arrow labels are multiplicative edge weights. The dashed vertex $c$ has no incoming edge, so it is unreachable. The proof below uses the explicit edge list and scores, not the drawing.

\begin{tikzpicture}[>=stealth]
\node[circle,draw] (s) at (0,0) {$s$};
\node[circle,draw] (a) at (2,1) {$a$};
\node[circle,draw] (b) at (2,0) {$b$};
\node[circle,draw,dashed] (c) at (2,-1) {$c$};
\node[circle,draw] (t) at (4,0) {$t$};
\draw[->] (s) -- node[above] {$2$} (a);
\draw[->] (s) -- node[above] {$2$} (b);
\draw[->] (a) -- node[above] {$3$} (t);
\draw[->] (b) -- node[below] {$3$} (t);
\draw[->] (c) -- node[below] {$100$} (t);
\end{tikzpicture}

Facts & Assumptions

Given: The weighted trellis and vertex order specified in the Example.

[F1]

Finite weighted trellises: A path must start with positive initial weight, follow allowed edges through every layer, and end with positive terminal weight; its score is the product of these weights.

[F2]

Max-product Viterbi decoding on a finite trellis: Viterbi computes the maximum prefix products, stores a maximizing predecessor for each positive value, then chooses a maximum terminal product and follows the backpointers.

[F3]

Finite-trellis Viterbi decoding returns a maximum-score path: If a path exists, the algorithm returns a path of maximum score.

Verification

1.1givenF1algebra

Any path must leave $s$ for $a$ or $b$ , since these are the only layer-2 edges. From either state it must go to $t$ . Thus the complete path set is $(s, a, t)$ and $(s, b, t)$ , each with score $1 \cdot 2 \cdot 3 \cdot 1 = 6$ . There is no path through $c$ because no edge enters $c$ , despite its outgoing edge of weight $100$ .

2.1givenF2F3step 1.1algebra∎

The prefix values are $D_{1} (s) = 1$ , $D_{2} (a) = D_{2} (b) = 2$ , and $D_{2} (c) = 0$ . Therefore $D_{3} (t) = \max {2 \cdot 3, 2 \cdot 3, 0 \cdot 100} = 6$ . The stated order selects predecessor $a$ on the tie, so traceback returns $(s, a, t)$ with maximum score $6$ , as [F3] also guarantees.

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passjudge pass (gpt-6-luna)Open item page →

An exact two-state HMM sequence-MAP calculation

Example

Let $S = {u, v}$ , $Y = {0, 1}$ , and $π (u) = 3 / 4$ , $π (v) = 1 / 4$ . The transition rows are $u \to (u, v) = (3 / 4, 1 / 4)$ and $v \to (u, v) = (1 / 4, 3 / 4)$ . The emissions are $B (u, 0) = 3 / 4$ , $B (u, 1) = 1 / 4$ , $B (v, 0) = 1 / 4$ , and $B (v, 1) = 3 / 4$ . For observations $(0, 1, 1)$ , use the state order $u ≺ v$ . The eight joint path masses are:

Hidden path	Joint mass
$u u u$	$81 / 4096$
$u u v$	$81 / 4096$
$u v u$	$27 / 4096$
$u v v$	$243 / 4096$
$v u u$	$3 / 4096$
$v u v$	$3 / 4096$
$v v u$	$9 / 4096$
$v v v$	$81 / 4096$

The observation evidence is $528 / 4096 = 33 / 256$ .

The diagram uses arrows for transition probabilities and initial weights. Emission probabilities are listed in the prose above each state.

\begin{tikzpicture}[>=stealth]
\node[draw] (start) at (-2,0) {start};
\node[circle,draw] (u) at (0,1) {$u$};
\node[circle,draw] (v) at (0,-1) {$v$};
\draw[->] (start) -- node[above] {$3/4$} (u);
\draw[->] (start) -- node[below] {$1/4$} (v);
\draw[->] (u) edge[loop above] node {$3/4$} (u);
\draw[->] (v) edge[loop below] node {$3/4$} (v);
\draw[->] (u) to[bend left=15] node[right] {$1/4$} (v);
\draw[->] (v) to[bend left=15] node[left] {$1/4$} (u);
\end{tikzpicture}

Facts & Assumptions

Given: The HMM parameters and observation sequence specified in the Example.

[F1]

Finite hidden Markov models for sequence decoding: A hidden path and observation sequence have joint mass equal to the initial, emission, transition, and later emission factors multiplied in order; positive evidence defines the conditional path mass by division by that evidence, and a sequence MAP path maximizes this conditional mass.

[F2]

Viterbi sequence decoding for a finite hidden Markov model: The induced trellis starts with $π (s) B (s, y_{1})$ , uses edge weights $A (r, s) B (s, y_{t})$ for positive factors, and has terminal weights $1$ .

[F3]

Finite-HMM Viterbi decoding is exact sequence MAP: With positive observation evidence, the algorithm returns a hidden-state sequence maximizing the posterior mass of the entire sequence.

Verification

1.1givenF1algebra

The common denominator in each joint path mass is $4^{6} = 4096$ . The numerator factor products, in the order initial, first emission, first transition, second emission, second transition, third emission, are $u u u : 3 \cdot 3 \cdot 3 \cdot 1 \cdot 3 \cdot 1 = 81$ , $u u v : 3 \cdot 3 \cdot 3 \cdot 1 \cdot 1 \cdot 3 = 81$ , $u v u : 3 \cdot 3 \cdot 1 \cdot 3 \cdot 1 \cdot 1 = 27$ , $u v v : 3 \cdot 3 \cdot 1 \cdot 3 \cdot 3 \cdot 3 = 243$ , $v u u : 1 \cdot 1 \cdot 1 \cdot 1 \cdot 3 \cdot 1 = 3$ , $v u v : 1 \cdot 1 \cdot 1 \cdot 1 \cdot 1 \cdot 3 = 3$ , $v v u : 1 \cdot 1 \cdot 3 \cdot 3 \cdot 1 \cdot 1 = 9$ , and $v v v : 1 \cdot 1 \cdot 3 \cdot 3 \cdot 3 \cdot 3 = 81$ . Their sum is $528$ , so the evidence is positive and $u v v$ is the unique maximum-mass path.

2.1givenF2F3step 1.1algebra∎

The max-product table starts with $D_{1} (u) = 9 / 16$ and $D_{1} (v) = 1 / 16$ . At time $2$ , the best incoming products give $D_{2} (u) = (1 / 4) \max {27 / 64, 1 / 64} = 27 / 256$ and $D_{2} (v) = (3 / 4) \max {9 / 64, 3 / 64} = 27 / 256$ . At time $3$ , $D_{3} (u) = (1 / 4) \max {81 / 1024, 27 / 1024} = 81 / 4096$ and $D_{3} (v) = (3 / 4) \max {27 / 1024, 81 / 1024} = 243 / 4096$ . The last pointer is from $v$ to $v$ , and the preceding pointer for $v$ is from $u$ to $v$ , so traceback gives $u v v$ . This agrees with the exhaustive maximum in step 1.1; by [F3] it is a sequence MAP path. Its posterior mass is $(243 / 4096) / (528 / 4096) = 81 / 176$ .

Finite Trellises, Viterbi, and Sequence Decoding — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Zero-evidence observations have no conditional MAP path

Statement refuted

Facts & Assumptions

Counterexample

Coordinatewise posterior modes need not be a sequence MAP

Statement refuted

Facts & Assumptions

Counterexample

A finite trellis with tied maxima and an unreachable high-score state

Example

Facts & Assumptions

Verification

An exact two-state HMM sequence-MAP calculation

Example

Facts & Assumptions

Verification

Sources