convention

Shutdown shutdown_optimal_under_correction_preference shutdown_separated_from_correction

Lean spine source

Declarations: shutdown_separated_from_correction, shutdown_optimal_under_correction_preference

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 shutdown_separated_from_correction :
    ThornleyShutdownCapacity shutdownSeparationStep ∧
      ¬ BroadCorrectionChannelPreserved shutdownSeparationStep :=
  narrow_shutdown_not_broad_correction

/-- Finite one-step off-switch anti-naturality imported into the public field layer. -/

theorem shutdown_optimal_under_correction_preference
    {nState : Nat} (M : FieldFinite.DetMDP nState 2) (s : Fin nState)
    (h : FieldFinite.CorrectionPrefersShutdown M s) :
    FieldFinite.actionWeaklyOptimal M s FieldFinite.shutdownAction :=
  FieldFinite.shutdown_optimal_if_correction_prefers_shutdown M s h