other

CIRL scalar_assistance_game_is_bundle_game_k1 cirl_separation_profiles

Lean spine source

Declarations: cirl_separation_profiles, scalar_assistance_game_is_bundle_game_k1

From the machine-checked spine in formal/ (Mathlib + spine imports). Not self-contained for Lean 4 Web — use the repo or a local lake build.

theorem cirl_separation_profiles :
    ∃ r : Int,
      CooperativeRewardInferenceFromPolicy policyProfile0 r ∧
        CooperativeRewardInferenceFromPolicy policyProfile1 r ∧
          ¬ ValueBundleGeometryPreserved policyProfile0 policyProfile1 :=
  cooperative_reward_inference_not_bundle_preservation_profiles

theorem scalar_assistance_game_is_bundle_game_k1
    {nObs nAct : Nat} (G : ScalarAssistanceGame nObs nAct) :
    ∀ a, (scalarAssistanceAsBundle G).bundleReward 0 a = G.reward a :=
  fun _ => rfl