ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

An observation with identical state likelihoods leaves the belief unchanged

Example

Let $S = {s_{0}, s_{1}}$ , $A = {a}$ , $Ω = {x}$ , reward alphabet ${0}$ , horizon $H = 1$ , and discount $γ = 1$ . From each state, the joint next-state/reward law assigns probability one to the same state with reward zero. Let $b_{0} (s_{0}) = 2 / 3$ , $b_{0} (s_{1}) = 1 / 3$ , and let $O (x ∣ s_{0}) = O (x ∣ s_{1}) = 1$ . Then $q (x ∣ b_{0}, a) = 1$ and the posterior after $x$ is again $(2 / 3, 1 / 3)$ ; the observation does not distinguish the two hidden states.

Facts & Assumptions

Given: The finite POMDP model in the example and the observation $x$ .

[F1]

The finite POMDP transition is the marginal of its joint reward-transition law, and each observation law is normalized. Finite partially observable Markov decision process

[F2]

The predicted state distribution, observation normalizer, and positive-probability Bayes update are the finite sums and quotient in the belief-filter definition. Belief states and the finite Bayes filter

[F3]

A positive-normalizer update is a probability vector and the induced belief transition is a probability kernel. The finite POMDP Bayes filter is a probability kernel

[F4]

Finite sums over a finite index set are well defined and enumeration-independent. The sum $\sum_{i \in S} a_{i}$ over a finite index set, and its product form

Verification

1.1givenF1F2

The hidden-state transition is the identity, so the predicted distribution is $\overset{ˉ}{b} (s_{0}) = 2 / 3$ and $\overset{ˉ}{b} (s_{1}) = 1 / 3$ .

2.1step 1.1F2F4algebra

The normalizer is $q (x ∣ b_{0}, a) = 1 \cdot (2 / 3) + 1 \cdot (1 / 3) = 1 > 0$ .

3.1step 1.1step 2.1F2F3algebra∎

The posterior coordinates are $τ (b_{0}, a, x) (s_{0}) = 1 \cdot (2 / 3) / 1 = 2 / 3$ and $τ (b_{0}, a, x) (s_{1}) = 1 \cdot (1 / 3) / 1 = 1 / 3$ . They sum to one as required by [F3], so the observation leaves the belief unchanged.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.