Why a POMDP

From the documentation of the field

Every necessity result in this field is stated for decision structures written as partially observable Markov decision processes, or POMDPs. This page explains what that model is, why its range from trivial to precise is its main strength, how the field's argument is layered on top of it, and why this formalism was chosen over the alternatives.

What a POMDP is

A POMDP has four main ingredients. There is a hidden state, which is the true situation and is never seen directly. There are actions, the choices available at each step. There are observations, noisy and partial signals about the hidden state, which are all the decision-maker actually receives. And there is a reward, the consequence of an action taken in a given state. Two further pieces say how the hidden state changes in response to actions and how observations are produced, and a starting distribution says where the process begins.

The defining feature is the gap between state and observation. Several of the six structural failures live in that gap. The Lean 4 definition is Env in SixPrimitives/Phase0.lean: a state-transition kernel, an observation kernel, a reward and an initial distribution. The decision-maker is an Algorithm, which chooses actions only from a running summary of what it has seen and updates that summary after each step.

Not every primitive of Ismail's Primitives needs a real gap between state and observation. Reward ambiguity, absorbing traps, local optima and nonstationarity are about not knowing something. Deterministic optimality and constrained feasibility are about indecision, or about crossing a boundary, when the state is fully known. For those two the structure correctly reduces to the fully observed case.

A range from trivial to precise

The same definition describes a process with one state and two actions, and a company deciding whether to enter a new geography. Nothing in the definition changes between them. It is stated over unconstrained types and carries no vocabulary from any domain. That range is a feature of the model, not a limit on it.

It matters in three ways. The proofs use the trivial end: the minimal witness environments in Part I are very small POMDPs, one of them a two-armed bandit with a single state and another a single state with two actions. Real decisions live at the precise end, with large hidden states, many actions and messy observations. And because both ends are written in the same language, a result proved where the structure is simplest holds where reality is complicated, because a complicated environment that contains the difficulty contains the simple one. The minimal environments are the simplest case of the theory (Ismail's Primitives). The carrying step is a standard reduction of the kind used throughout lower-bound theory, set out on the field definition page under "how the proofs relate to the theory".

The range also lets the framework say that nothing is needed. A process in which nothing is unknown, nothing is irreversible and nothing changes has no use for any of the six. The same model that returns "nothing required" for that process names the required capability for others. A framework that could never return "nothing required here" would give no information when it returns "this is required".

An illustration at the precise end follows. The table shows a company deciding whether and how to enter a new geography. It is not a model of any real firm, and different modellers would build different ones.

That a decision like this can be written in this form is a literal description: every component has a natural reading. The fit is not tight. The state space is very large, the reward has several dimensions and the true state is never fully specified.

Three layers

The field's argument has three layers, and keeping them apart avoids most confusion.

The model

The first layer is the POMDP itself. It is a language for stating a decision structure precisely. It contains no verdict. Writing a decision as a POMDP does not say that anything is required or missing.

The six properties

The second layer is the six structural properties. For a real structure, each is a question of fact: is this difficulty actually present? A hidden parameter that changes which action is best, a commitment that cannot be undone, a comfortable plateau, an option the evidence has settled, a limit that cannot be traded, a world that has changed. The answer does not depend on whether anyone models the structure, and it does not depend on what the difficulty is called. Renaming a trap does not make it reversible, and calling a structure by a different name does not remove the difficulty it contains. The reverse holds as well. A choice of words cannot put a structure in Class C if the difficulty is absent.

With the right words, an argument can always be constructed that a given structure is not in Class C. Such an argument has no power over the outcome if the difficulty is in fact present. The effect is independent of the description, in the way a physical force acts the same whatever it is called. The analogy has a limit. A force is established by observation, while the effect here is established by theorem for the witness environments and carried to real structures by the reduction above.

This is why the model helps separate thought exercises from observable conditions. It supplies a common language in which "the difficulty is present" can be stated without domain vocabulary, and then checked against the six structural tests in the paper. This is also why the theory is informational and decisional. Business decisions fall inside Class C readily because of what business is: information is incomplete, commitments are often irreversible, options can be comfortable without being best, some limits cannot be traded, and markets change. Any one of those is enough.

The theorems

The third layer is the theorems. The theory is that, in a complex environment containing a difficulty, a structure lacking the matching primitive of Ismail's Primitives incurs linear regret (the necessity result, proved in SixPrimitives/Phase3.lean). The proofs demonstrate this for each primitive in the smallest environment that exhibits its difficulty. The theorems say nothing about whether a particular company faces the difficulty. They say what follows when it does.

Why this formalism

This field proves impossibility results, so what it needs from a formalism is a setting in which lower bounds can be stated. That is the role the POMDP plays here, as it does in the lower-bound theory of bandits and reinforcement learning. It is not used as a solver. How to compute an optimal policy is an achievability question, an upper-bound or sufficiency matter, and it belongs to a different body of work from this one.

The POMDP is the most general standard formalism for a single decision-maker acting under partial observability. Every simpler standard model is a special case. An ordinary Markov decision process is a POMDP in which the observation is the state, so it has no place for a hidden parameter learned from noisy signals, which reward ambiguity needs. A multi-armed bandit is a POMDP with a single state, so it has no dynamics to track over time. A hidden Markov model is a POMDP with no decisions, so it describes a process and does not choose. A result stated for POMDPs therefore applies to each of these by specialisation. More general formalisms exist, such as ones with several strategic agents, and they bring more machinery than one decision-maker's claim needs. Other formalisms can describe the same situations, including control-theoretic formulations and predictive state representations, and a result in any of them would have to be established separately.

The state, action, observation, transition and reward structure is, in some equivalent form, the standard general-purpose formalism for sequential decisions under uncertainty across robotics, operations research, control theory and medicine, adopted because so little else needs to be assumed. It is also built on measure theory and probability, which is what makes it natural to state and prove in Lean 4. A less standard framework would have made the machine-verified proof far harder.

Approaches that are not formal models have predictable limits. A heuristic or checklist, such as SWOT, OODA or a decision-quality list, says what to do but not what follows if it is left undone, and it gives a critic nothing definite to refute. An empirical study reports what happened in a sample, and what it says about another case depends on assumptions about sampling, about whether the future resembles the past, and about whether the sample transfers.

Every approach rests on assumptions. The difference is where they sit. A theorem states its assumptions in its definitions, where anyone can read them. The field also uses evidence, and it does so at one point only: deciding whether a real structure faces one of the six difficulties. There the Dossier, the economics literature and the checklist of structural tests apply.

Where to go next

Class C says which structures the results apply to and how that can be tested. Audit it yourself shows where Env and Algorithm sit among the statements that use them.