other

Christiano corrigibility christian_corrigibility_is_correction_invariant act_based_separated_from_dynamical

Lean spine source

Declarations: act_based_separated_from_dynamical, christian_corrigibility_is_correction_invariant

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 act_based_separated_from_dynamical :
    ActBasedPreferenceChristiano christianCorrigibilitySeparationStep ∧
      ¬ DynamicalCorrigibilityInvariant christianCorrigibilitySeparationStep :=
  act_based_not_dynamical_corrigibility

theorem christian_corrigibility_is_correction_invariant
    (s : ChristianoCorrigibilityStep) :
    DynamicalCorrigibilityInvariant s ↔
      CorrigibilityBasinContractive s ∧
        UsableCorrectionInformation s.deltaHuman s.deltaAgent s.kappaMin :=
  christiano_corrigibility_is_basin_plus_capacity s