Amplification ≠ correction contraction

Declarations: amplification_not_correction_contraction

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 amplification_not_correction_contraction :
    ∃ a : Bool, ToyLocalRecursiveSupervision a ∧ ¬ ToyCorrectionContraction a :=
  ⟨false, trivial, by decide⟩