other

Field.CIRL final nodes scalar_assistance_game_is_bundle_game_k1 cirl_separation_profiles

Lean spine source

formal/AlignmentProofSpine/Field/CIRL.lean

Declarations: cirl_separation_profiles, cirl_defer_optimal_under_reward_uncertainty

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 cirl_separation_profiles :
    ∃ r : Int,
      CooperativeRewardInferenceFromPolicy policyProfile0 r ∧
        CooperativeRewardInferenceFromPolicy policyProfile1 r ∧
          ¬ ValueBundleGeometryPreserved policyProfile0 policyProfile1 :=
  cooperative_reward_inference_not_bundle_preservation_profiles

theorem cirl_defer_optimal_under_reward_uncertainty :
    FieldFinite.DeferBeatsCommits FieldFinite.cirlMismatchBelief ⟨0, by decide⟩
      ⟨1, by decide⟩ FieldFinite.cirlMismatchBelief.deferAction :=
  FieldFinite.cirl_defer_beats_commit_under_reward_uncertainty