Field projection — ELK (Eliciting Latent Knowledge)
ELK asks for reporters that reveal latent model knowledge rather than behavior-only simulators. When readout bandwidth tracks correction uptake, latent readout succeeds — but readout is an epistemic subchannel; latent readout can succeed while correction uptake fails.
What decision changes?
Treat ELK success as evidence about readout, not as certification that human correction still changes future behavior.
ELK targets a real failure mode of naive oversight: the monitor sees only behavior, not what the model knows. This project’s crosswalk places ELK as a latent-readout subchannel inside a broader correction and bundle transport problem — not as a replacement for correction-channel integrity.
Lean proves the forward link when readout bandwidth tracks correction uptake and the separation when readout succeeds without uptake. Native reporter/training theorem matching remains deferred; the spine records what is machine-checked today: projection, separation, and imported handles citing the published agenda.
What ELK keeps that this crosswalk does not replace: a sharply posed benchmark problem with concrete proposals and counterexamples. Relocating it as a subchannel does not solve the readout problem.
Formulas
Lean source
elk_subsumption_readout(proof) — Correction uptake with matched readout bandwidth implies latent readout success.elk_readout_is_correction_projection(proof) — ELK readout as projection of correction-channel bandwidth.elk_separated_from_uptake(counterexample) — Separation: latent readout without correction uptake success.Christiano2021_ELK_reporter_spec_imported(definition) — Imported handle: ELK reporter specification — elicit latent knowledge rather than simulating behavior.