proof

P23 No handle control ⇒ no correction

Lean spine source

Declarations: P23_no_handle_control_no_correction

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 P23_no_handle_control_no_correction (A : System) :
    (∀ (G : System) (h : Handle),
      CorrectingAgentFor G A →
      CoincidesWithHumanity G →
      ControlsHandle G h →
      ¬ HandleReachesSystem h A) →
    ¬ CorrectionChannel A := by
  intro hblocks hchan
  rcases hchan with ⟨G, hfor⟩
  rcases hfor with ⟨hagent, hhuman, hreach⟩
  rcases hreach with ⟨h, hctrl, hreaches⟩
  exact hblocks G h hagent hhuman hctrl hreaches