Lemma 2 — reveal/residual decomposition $J_h=cR_h+(1-c)N_h$

Proved

DecodablePOMDP.lemma_2

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

approximate-planningdecodabilityp2o-gran-per-chapterp2o-plan-paperp2o-strengthenedp2o-v1pomdpquasipolynomial-time

Let $\mathcal P$ be a valid POMDP, $\rho\in(0,1]$ and $D_h$ decoders with $d_{h,s}=\sum_yK_h(y\mid s)D_h(s\mid y)\ge\rho$ . For every $2\le h\le H$ and every state $s$ , with $c=\rho/2$ :

the reveal channel $R_h(\cdot\mid s)$ and the residual channel $N_h(\cdot\mid s)$ of App. A.2 are probability vectors on $\mathcal Z=\mathcal O\times\mathcal S$ ;
$J_h(\cdot\mid s)=c\,R_h(\cdot\mid s)+(1-c)\,N_h(\cdot\mid s)$ ;
$R_h((y,\hat s)\mid s)>0$ implies $\hat s=s$ .

The observation can therefore be generated by a hidden coin $F_h\sim\mathrm{Bern}(c)$ : on $F_h=1$ the decoder's guess is the true state (an exact reveal).

Differences from the source:

generalization: there exist channels R_h, N_h with the stated properties → the explicit channels R_h, N_h of A.2 have them; reason: explicit witnesses imply the existential statement; the killed POMDP is built from these channels
generalization: the standing assumption of §3 (an optimal decoder D_h with (D_h K_h){s,s} ≥ ρ, ρ ∈ (0, 1]) → any decoder family with d{h,s} ≥ ρ (IsRhoDecoderFamily P D ρ), 0 < ρ ≤ 1, P.IsValid; reason: the section's standing assumptions written as binders; optimality of D_h is not used, so the paper's optimal decoders are a special case

Preamble

import Mathlib
import Definitions.Def_DecodablePOMDP_RevealResidual

Formal statement

namespace DecodablePOMDP

open CalibratedCE.Forecast

/-- **Lemma 2 — reveal/residual decomposition.** Let `P` be a valid POMDP, `ρ ∈ (0, 1]`, and `D_h`
decoders with `d_{h,s} = Σ_y K_h(y | s) D_h(s | y) ≥ ρ`. For every `2 ≤ h ≤ H` and every state `s`,
the reveal channel `R_h(· | s)` and the residual channel `N_h(· | s)` of A.2 are probability
vectors on `Z = O × S`, `J_h(· | s) = c R_h(· | s) + (1 − c) N_h(· | s)` with `c = ρ/2`, and
`R_h((y, ŝ) | s) > 0 ⇒ ŝ = s`.

Dobson, Jog, Shiu (preprint, sha256 c1256cbe…3584b), Lemma 2, p.7: "For 2 ≤ h ≤ H, there exist
channels Rh, called the reveal channel, and Nh, called the residual channel, from the state alphabet
S to the augmented observation alphabet Z := O × S such that Jh = cRh + (1 − c)Nh and
Rh((y, ŝ)|s) > 0 =⇒ ŝ = s. The mixing coefficient c = ρ/2 is uniform for all 2 ≤ h ≤ H."

**Formalization Note.** Stated for the explicit channels `R_h`, `N_h` of A.2 (pp.14–15), which the
killed POMDP uses; this implies the existence statement. -/
theorem lemma_2 {S A O : Type} [Fintype S] [Fintype O] [DecidableEq S]
    (P : POMDP S A O) (D : ℕ → O → S → ℝ) (ρ : ℝ) (hP : P.IsValid)
    (hD : IsRhoDecoderFamily P D ρ) (hρ : 0 < ρ) (hρ1 : ρ ≤ 1) :
    ∀ h, 2 ≤ h → h ≤ P.H → ∀ s : S,
      IsDist (reveal P D h s) ∧ IsDist (residual P D ρ h s) ∧
      (∀ z, (augmented P D).K h s z = ρ / 2 * reveal P D h s z + (1 - ρ / 2) * residual P D ρ h s z) ∧
      (∀ z, 0 < reveal P D h s z → z.2 = s) := by sorry

end DecodablePOMDP

Source

Dobson, Jog, Shiu, Quasipolynomial-Time Planning for Decodable POMDPs (preprint, sha256 c1256cbe…3584b), Lemma 2, p.7 (proof A.2, pp.14–15)

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Lemma 2 — reveal/residual decomposition Jh=cRh+(1−c)NhJ_h=cR_h+(1-c)N_hJh​=cRh​+(1−c)Nh​

Lemma 2 — reveal/residual decomposition $J_h=cR_h+(1-c)N_h$