Towards Superintelligence Alignment
other

Lean proof spine

FCIRL

Lean spine source

formal/Field/CIRL.lean

Declarations: cirl_separation_profiles, cirl_defer_optimal_under_reward_uncertainty

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 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