# Continue K-COS end-to-end work

Use this checkpoint's `lean/` tree and `verification/accepted/run.json`. Do not restart from the 26-theorem publication companion or overwrite the frozen monograph.

Read `docs/PROGRESS_LEDGER.md`, `docs/END_TO_END_TARGET.md`, and `docs/COVERAGE.json` first. The new central Gaussian, matrix/spectral, stochastic-coupling, and rational-acceptance links are present. The final composition theorem still requires valid numerical spectral bounds and endpoint probability bounds.

The next module is `KomorebiQCOS/TiltedMeasure.lean`: define the actual exponential tilt from a density, prove normalization, and derive the change-of-measure identity. Do not assume that identity or treat a preexisting numerical Boolean as a theorem.

Use the stored exact-pin Lean runtime. `docs/RUNTIME_RECOVERY.md` identifies the five archive parts and the verified combined hash. `python verify.py --runtime PATH` runs an isolated verification without replacing accepted evidence.