Is scalar CIRL enough?

Cooperative inverse reinforcement learning (CIRL) asks a robot to infer a human's reward from interaction and act to maximize cooperative return. The field object is usually scalar: one reward coordinate to learn.

This project's target is bundle inference — multiple value directions, bearer maps, and transport that survives representation change. Scalar CIRL is the k = 1 embed: lifting a single reward to a constant bundle coordinate (`scalar_assistance_game_is_bundle_game_k1`).

Short answer: Scalar CIRL is a strict projection, not the full problem. Lean proves full finite transport implies cooperative reward inference (forward), and proves the separation: cooperative scalar inference can hold while bundle geometry fails to preserve across profiles that share the same scalar marginal (`cirl_separation_profiles`).

Lean does not prove that real CIRL training finds the intended bundle, or that assistance-game optimality carries over under optimization pressure — those remain field stories plus MB2/MB3 bridges.

Field terms

• cooperative inverse reinforcement learning
• scalar reward inference
• assistance games
• bundle inference

Stepping-stone path

Read in order — each step adds one book term, not the whole ontology.

1. cirl
2. value bundle transport
3. bundle identifiability
4. bearer import

What Lean checked (forward)

• scalar_assistance_game_is_bundle_game_k1 — Lean source · Spine node
• cirl_subsumption_forward — Lean source

What Lean checked (separations)

• cirl_separation_profiles — Lean source · Spine node counterexample