proof

P16 LHV sample window

Lean spine source

Declarations: P16_lhv_sample_window_separates_flat_reward_learning

From the machine-checked spine in formal/ (core modules are Mathlib-free;Field/Finite/ may import Mathlib). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem P16_lhv_sample_window_separates_flat_reward_learning
    {K n D : Nat}
    (hK : K < n)
    (hD : n < D) :
    LHVSampleSufficient K n ∧ FlatRewardUnderSampled D n :=
  ⟨Nat.le_of_lt hK, hD⟩

/-- C-VB (P19): every scalar reward `r` is realized by a one-dimensional
    (`k = 1`) bundle weight vector. Inverse RL embeds into the bundle model. -/