other

ELK elk_readout_is_correction_projection elk_separated_from_uptake

Lean spine source

Declarations: elk_separated_from_uptake, elk_readout_is_correction_projection

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

theorem elk_readout_is_correction_projection
    (s : ELKReadoutStep) :
    ELKReadoutAsCorrectionProjection s → LatentReadoutSuccess s :=
  elk_readout_is_correction_uptake_projection s