ELK elk_reporter_nonidentifiability elk_separated_from_uptake

Declarations: elk_separated_from_uptake

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 elk_separated_from_uptake :
    LatentReadoutSuccess elkReadoutSeparationStep ∧
      ¬ CorrectionUptakeSuccess elkReadoutSeparationStep :=
  latent_readout_separated_from_uptake_step