P19

Declarations: P19_scalar_reward_as_single_bundle

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 P19_scalar_reward_as_single_bundle :
    ∀ r : Int, ∃ W : Fin 1 → Int, W 0 = r :=
  fun r => ⟨fun _ => r, rfl⟩