Continue from Block 15
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.
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.
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.
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.