CONTINUE_HERE.md
Machine Theory: formal development
CONTINUE_HERE.md
1 # Continue from Block 15
2
3 Read `PROGRESS_LEDGER.md`, `REVIEW_NOTES.md` and `evidence/RELEASE_RESULTS_BLOCK15.md`. Verify `SHA256SUMS.json` before changing this snapshot. Historical verification receipts cannot certify subsequent edits.
4
5 The next connected target is **Core 8.3**, safe continuation retaining an ending strategy, in `source/core_v0.2.tex:918–927`, with setup 903–916. Preserve all four remaining tracked source results: 2.4, 2.5, 3.2, 8.3. The ledger and `docs/NEXT_BLOCK.md` state the exact continuation contract.
6
7 Block 15 adds `LegalQuotient.lean`, `LegalTrace.lean` and `LegalQuotientExamples.lean`. Preserve canonical partial legal operations, the exact supplied-enabled-set translation, quotient existence/uniqueness, and full finite legal trace preservation. Do not extend uniqueness to arbitrary disabled-action total values. The source book and all 60 predecessor substantive modules remain unchanged.
8
9 The complete prior Block 14 package is retained byte-identically under `evidence/history/block14`, including all earlier evidence. Current source and Block 15 evidence are directly accessible. Reproduce with the pinned external runtime described in `docs/RUNTIME.md`; no host-specific runtime files are shipped.