CONTINUE_HERE.md
COS Method: formal continuation
CONTINUE_HERE.md
1 # Continue K-COS end-to-end work
2
3 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.
4
5 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.
6
7 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.
8
9 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.