ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

A finite POMDP family has exponentially many witnessed alpha vectors

Example

For each $n \in N$ with $0 < n$ , let $I_{n} = {t \in N : t < n}$ be a clock set and let a hidden binary string be a function $x : I_{n} \to {0, 1}$ . Write $σ (t)$ for the natural successor. Put $S = {(x, t) : x \in {0, 1}^{I_{n}}, t \in I_{n}}$ , $A = {0, 1}$ , $Ω = {o}$ , and reward alphabet $R = {0, 1}$ . For $t \in I_{n}$ , define $t^{+} = σ (t)$ if $σ (t) \in I_{n}$ , and $t^{+} = t$ otherwise. Under action $a$ at $(x, t)$ , the joint next-state/reward law assigns probability one to next state $(x, t^{+})$ and reward $1_{{a = x (t)}}$ ; the sole observation $o$ occurs with probability one. Let $x^{\circ} : I_{n} \to {0, 1}$ be the constant-zero string, take $b_{0} = δ_{(x^{\circ}, 0)}$ , and set horizon $H = n$ and $γ = 1$ . There are exactly $2^{n}$ depth- $n$ policy trees, one for each binary action string $y : I_{n} \to {0, 1}$ . The alpha vector of tree $y$ , evaluated at state $(x, 0)$ , is $\sum_{t < n} 1_{{x (t) = y (t)}}$ . At the point-mass belief $δ_{(y, 0)}$ this vector has value $n$ , while every distinct action string has value strictly less than $n$ . Therefore all $2^{n}$ alpha vectors are distinct and each has a witness belief in $Δ (S)$ , which need not be reachable from the specified initial belief; the family has state count $n 2^{n}$ .

Facts & Assumptions

Given: A natural number $n$ with $0 < n$ and the finite POMDP described in the example, with initial belief $δ_{(x^{\circ}, 0)}$ , horizon $n$ , and discount $1$ .

[F1]

A finite POMDP has finite state, action, and observation sets, transition and observation probability laws, an initial belief, and a finite-horizon objective. Finite partially observable Markov decision process

[F2]

A depth-zero tree has vector $0$ ; a depth- $(h + 1)$ tree consists of a root action and one subtree per observation, with vector given by the finite transition-observation backup. Exhaustive finite-horizon POMDP alpha-vector backup

[F3]

The value at horizon $H$ is the maximum of $b \cdot α$ over the backup's vectors, and a vector is witnessed when it attains that maximum at some belief. Finite-horizon POMDP values are piecewise-linear and convex

[F4]

For finite sets, the function set $X^{Y}$ is finite of cardinality $∣ X ∣^{∣ Y ∣}$ . The set $A^{B}$ of functions $B \to A$ between finite sets is finite, with $∣ A^{B} ∣ = ∣ A ∣^{∣ B ∣}$

[F5]

Finite Cartesian products are finite and their cardinalities multiply; cardinality is the natural number equinumerous with the set. The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , The cardinality $∣ A ∣$ of a finite set

[F6]

Natural powers start at $m^{0} = 1$ and satisfy $m^{h + 1} = m^{h} m$ . Exponentiation of natural numbers, $m^{n}$ , and its agreement with the integer power in $R$

[F7]

Finite sums over an initial segment are recursively defined and preserve termwise inequalities. Finite sums and finite products, by recursion, Laws of finite sums and finite products

[F8]

A belief is a probability vector on $S$ , so the point mass at any state of $S$ is a belief. Belief states and the finite Bayes filter

[F9]

In the von Neumann naturals, $0 \in n$ when $n \neq 0$ , $k \in σ (k)$ , every natural number is transitive, and $σ$ is the successor used by the clock. The natural numbers $N$ (von Neumann), On $N$ the order is membership: $m < n ⟺ m \in n$ , Every natural number is a transitive set and is not a member of itself

[F10]

The clock set $I_{n} = {t \in N : t < n}$ equals the von Neumann natural $n$ , so it is finite and has cardinality $n$ . A finite initial segment of the naturals has its index as cardinality

[F11]

If a property holds at $0$ and its truth at $k$ implies its truth at $σ (k)$ for every $k \in N$ , it holds for every natural number. The principle of mathematical induction

Verification

1.1givenF1F4F5F6F9F10

By [F10], $I_{n}$ is finite with cardinality $n$ . Hence the function set ${0, 1}^{I_{n}}$ has cardinality $2^{n}$ by [F4] and [F6], and the product rule [F5] gives $∣ S ∣ = n 2^{n}$ . Since $0 < n$ , [F9] gives $0 \in I_{n}$ , so $(x^{\circ}, 0) \in S$ and its point mass is a probability distribution. The action, observation, and reward sets are finite and nonempty. For each state and action the specified joint mass assigns one next-state/reward pair probability one, and the singleton observation law has total mass one; thus the data satisfy [F1].

1.2givenF3

With one observation, the tree-count recurrence in [F3] gives $N_{0} = 1$ and $N_{h + 1} = 2 N_{h}$ : each tree is determined by its root action and its unique observation continuation.

2.1step 1.2F4F6F11inductionalgebra

Induction using [F11] and the recursion for powers [F6] gives $N_{h} = 2^{h}$ for every $h$ : the base is $N_{0} = 1 = 2^{0}$ , and $N_{h + 1} = 2 N_{h} = 2 \cdot 2^{h} = 2^{h + 1}$ . A depth- $n$ tree with one observation is exactly an action string $y : I_{n} \to {0, 1}$ , so there are exactly $2^{n}$ such trees by [F4].

2.2givenstep 1.1F9F10F11induction

Let $c_{k}$ be the clock coordinate after $k$ transitions from the initial clock $0$ . We prove by induction that $k \in I_{n}$ implies $c_{k} = k$ . At $k = 0$ this holds. If $σ (k) \in I_{n}$ , then $k \in σ (k)$ by [F9], and transitivity of the natural $n = I_{n}$ from [F10] gives $k \in I_{n}$ ; the induction hypothesis gives $c_{k} = k$ . Since $σ (k) \in I_{n}$ , the transition rule advances to $c_{σ (k)} = σ (k)$ . If $σ (k) \notin I_{n}$ , the successor case of the implication is vacuous. The induction principle [F11] proves the claim for every $k$ .

3.1givenstep 2.2F1F2F7

Therefore, at each decision time $t \in I_{n}$ from initial state $(x, 0)$ , the hidden state is $(x, t)$ . Under the tree $y$ its reward at that time is $1_{{x (t) = y (t)}}$ , and the finite horizon sum with $γ = 1$ gives $α_{y} (x, 0) = \sum_{t < n} 1_{{x (t) = y (t)}}$ .

4.1givenstep 2.1step 3.1F3F7F8algebra∎

For each string $y$ , the point mass $δ_{(y, 0)}$ is a belief by [F8], and [F3] evaluates its tree there as $α_{y} (y, 0) = n$ . If $z \neq y$ , some coordinate $t$ differs, so the sum for $α_{z} (y, 0)$ has at least one zero term and all other terms at most one; its value is strictly less than $n$ . Thus $y$ is the unique maximizing tree at $δ_{(y, 0)}$ , so its vector is witnessed. If $y \neq z$ , their values at $δ_{(y, 0)}$ differ, so their vectors are distinct. By step 2.1 there are $2^{n}$ strings; hence the example has exactly $2^{n}$ distinct witnessed vectors.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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.