Mnehmos · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026
@@ -94,10 +94,12 @@ identities are intentionally distinct and both are verified.
 | `private` | `private_audit_only` | `private_only` | `private` |
 | `public` | `quarantined` | `quarantined` | `public`, with explicit source and module licenses |
 
-A private release is never promoted to a training split. A public release still remains
-quarantined because leakage-aware split assignment is a separate unfinished 1.0 capability.
-Public projection additionally requires source redistribution `allowed`, redaction `public`,
-and an explicit source and module license. Missing authority fails closed.
+A private release is never promoted to a training split. A public release remains quarantined in
+this corpus packet because the corpus exporter does not assign leakage-aware splits. The separate
+`rl_export_plan/1` projection must bind a verified public release to an eligible component-locked
+split; it does not retroactively change this packet's curation policy. Public projection also
+requires source redistribution `allowed`, redaction `public`, and an explicit source and module
+license. Missing authority fails closed.
 
 MCIP records are child evidence. They mirror a frozen kernel-verification result but cannot
 promote packet trust or replace the MathOS release, receipt, authority, or fidelity records.
@@ -108,4 +110,5 @@ The exporter emits the evidence MathOS can substantiate without guessing: `Packe
 canonical `ProofVariant`, and a `DependencyManifest`. It does not invent proof-search
 episodes, tactic counts, model identity, retrieval candidates, literature review, novelty,
 RL transitions, empirical difficulty, or leakage-aware train/validation/test assignments.
-Those remain separate tracked 1.0 work.
+Split assignment belongs to the separate RL/evaluation export; the other absent records remain
+tracked 1.0 work.
@@ -104,9 +104,11 @@ Phase 5 evidence: issue [#48](https://github.com/Mnehmos/MathOS/issues/48) adds
 
 Phase 6 portable-release evidence: issue [#50](https://github.com/Mnehmos/MathOS/issues/50) adds the closed Rust-owned `release_manifest/1` schema and a deterministic dry-run/new-directory builder rooted in one fully replayed publication receipt plus its persisted authority/current fidelity witness and one exact reviewed pedagogy path. Every required SPEC directory has manifest-bound members; exact record, logical/pedagogy edge, evidence, artifact, environment, publication, replay, report-copy, and license relationships are checked without SQLite. Private members retain explicit restrictions, and the public release profile rejects any restricted, private, or unlicensed member. Unit coverage reproduces the preview hash after restart, blocks overwrite and public projection, hides SQLite, revalidates the directory, and rejects extra files, expected-hash substitution, and a changed export. The protected Pilot A workflow builds five reviewed training-ineligible units, copies the resulting release, hides `state.sqlite3`, invokes verification with a nonexistent instance root and trusted manifest hash, replays the exact repaired theorem under Lean 4.32.0, and retains both bundle and report.
 
-Phase 6b corpus-export evidence: issue [#54](https://github.com/Mnehmos/MathOS/issues/54) and PR [#55](https://github.com/Mnehmos/MathOS/pull/55) pin the byte-exact Apache-2.0 MathCorpus packet and minimum MCIP v1 schemas at upstream commit `a0d08c9ace0dcc70a8bc281dcf29c560242075d3`, add the closed Rust-owned `corpus_export_manifest/1` contract, and expose database-independent `mcl release export` and `verify-export`. Classification is explicit rather than guessed. Private releases produce only `private_audit_only` packets, `private_only` MCIP records, and private sensitive members; public releases remain quarantined and additionally require explicit public redistribution, redaction, and license authority. Verification checks a trusted export hash, exact inventory and schemas, canonical packet/record hashes, source/publication/environment/module bindings, and byte-identical deterministic reprojection from an independently supplied frozen release. Unit and CLI coverage blocks overwrite, missing-root/config coupling, invalid curation, extra files and directories, packet/schema substitution, and expected-hash substitution. Exact-head CI `29884823358`, merged-tree CI `29885040172`, and protected publication run `29885040178` passed. Downloaded artifact `8516235885` independently reproduced source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1`, corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, and packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`; all 12 files and 11 manifest members matched, no links existed, deterministic reprojection passed without SQLite, and upstream MathCorpus and MCIP validators reported zero errors and warnings with hash checks enabled. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.
+Phase 6b corpus-export evidence: issue [#54](https://github.com/Mnehmos/MathOS/issues/54) and PR [#55](https://github.com/Mnehmos/MathOS/pull/55) pin the byte-exact Apache-2.0 MathCorpus packet and minimum MCIP v1 schemas at upstream commit `a0d08c9ace0dcc70a8bc281dcf29c560242075d3`, add the closed Rust-owned `corpus_export_manifest/1` contract, and expose database-independent `mcl release export` and `verify-export`. Classification is explicit rather than guessed. Private releases produce only `private_audit_only` packets, `private_only` MCIP records, and private sensitive members; public releases remain quarantined and additionally require explicit public redistribution, redaction, and license authority. Verification checks a trusted export hash, exact inventory and schemas, canonical packet/record hashes, source/publication/environment/module bindings, and byte-identical deterministic reprojection from an independently supplied frozen release. Unit and CLI coverage blocks overwrite, missing-root/config coupling, invalid curation, extra files and directories, packet/schema substitution, and expected-hash substitution. Exact-head CI `29884823358`, merged-tree CI `29885040172`, and protected publication run `29885040178` passed. Downloaded artifact `8516235885` independently reproduced source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1`, corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, and packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`; all 12 files and 11 manifest members matched, no links existed, deterministic reprojection passed without SQLite, and upstream MathCorpus and MCIP validators reported zero errors and warnings with hash checks enabled. RL/evaluation export and leakage-aware splits were still unfinished at that checkpoint; Phase 6c evidence follows.
 
-Phase 6c is actively tracked by issue [#57](https://github.com/Mnehmos/MathOS/issues/57). Its implementation defines receipt-bound cohort dates, required leakage declarations, derived exact relationship keys, component-locked splits, private-held-out/public-split policy, six evidence-backed task families plus conditional pedagogy tasks, explicit family skips, and database-independent reprojection after the existing explicit Lean release-replay gate. The checkbox remains open until exact-head CI, merged-tree CI, the protected Pilot A held-out export, and independent artifact audit all pass. Decomposition, proof repair, generalization, frontier selection, Comparator, remaining pilots, and full 1.0 acceptance remain separate open work.
+Phase 6c leakage-aware RL/evaluation evidence: issue [#57](https://github.com/Mnehmos/MathOS/issues/57) and PR [#58](https://github.com/Mnehmos/MathOS/pull/58) add the closed Rust-owned plan, task, leakage-report, and export-manifest v1 contracts; receipt-bound chronology; required declared plus derived exact relationship keys; transitive component locking; private-held-out/public-split policy; six evidence-backed task families plus conditional pedagogy tasks; explicit family skips; and database-independent deterministic reprojection after the separate platform-bound release replay. Reviewed head `2d0c8fd0ec417ea0801d8995d4b93414fcf0a814` merged as `4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`. Exact-head CI `29889101827`, merged-tree CI `29889317590`, and protected publication run `29889317589` passed.
+
+Downloaded artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline verification bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export contains 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and the six claimed families. Independent audit found zero inventory/hash/policy/trust-reference/cross-claim/cross-split/reasoning-field findings and reproduced every byte without SQLite. This completes issue #57's scoped leakage-aware foundation, but the broad SPEC 19.2/30.6 checklist criterion stays open until decomposition, proof repair, generalization, and frontier selection are projected too. Comparator, remaining pilots, migration, and full 1.0 acceptance also remain open.
 
 ## Migration
 

@@ -24,9 +24,11 @@ Issue [#50](https://github.com/Mnehmos/MathOS/issues/50) completed the first Pha
 
 Issue [#54](https://github.com/Mnehmos/MathOS/issues/54) completed the focused Phase 6b slice through PR [#55](https://github.com/Mnehmos/MathOS/pull/55). Reviewed head `55711785dd8ed9303bd54a0e7f6308efdead8ad7` merged as `e977d7eb69bfc262510c276912ba5584f3514a44`, tree `5c65154dd7f45497ba8ed1f06820ca3332ee9a7d`. Exact-head CI run `29884823358` and merged-tree CI run `29885040172` passed all five required jobs. Protected publication run `29885040178`, job `88813765985`, passed the protected-ref gate, authority/fidelity chain, repaired proof, portable release, database-hidden corpus preview/build/copy/reprojection, and retention.
 
-Artifact `8516235885`, `publication-boundary-e977d7eb69bfc262510c276912ba5584f3514a44`, is 417,954 archive bytes with GitHub SHA-256 `55b4342eb03d19941d73086b6c44aae5083c834f824205a6138c7ddcdfe7d1d4`; it expands to 325 files and 770,532 bytes. Independent audit matched all 12 corpus-directory files, all 11 manifest member hashes and sizes, found no symbolic links, and confirmed byte-identical copied source manifest and Lean module. Source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1` reprojected exactly to corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`, 11 members, and 101,695 member bytes. The retained preview, build, verification, and playtest summary agree; MathOS offline verification and the pinned upstream packet and MCIP hash validators reported zero findings. RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.
+Artifact `8516235885`, `publication-boundary-e977d7eb69bfc262510c276912ba5584f3514a44`, is 417,954 archive bytes with GitHub SHA-256 `55b4342eb03d19941d73086b6c44aae5083c834f824205a6138c7ddcdfe7d1d4`; it expands to 325 files and 770,532 bytes. Independent audit matched all 12 corpus-directory files, all 11 manifest member hashes and sizes, found no symbolic links, and confirmed byte-identical copied source manifest and Lean module. Source release `7b002ffe0fcaeecd0fe745dcedd135442b7372985a0fac5b9ffbe03af4c691b1` reprojected exactly to corpus manifest `4cb348d8a446f800d74865909c8fff66b310c5cd0fbe6fb00f6830d0961ed705`, packet `690d7f8a18fad1fee415b5d6ad4efeaf154a2a7dc366b892967230d49db6c69d`, 11 members, and 101,695 member bytes. The retained preview, build, verification, and playtest summary agree; MathOS offline verification and the pinned upstream packet and MCIP hash validators reported zero findings. RL/evaluation export and leakage-aware splits were still unfinished at that checkpoint; Phase 6c evidence follows.
 
-Issue [#57](https://github.com/Mnehmos/MathOS/issues/57) tracks the active Phase 6c implementation. The branch defines closed RL plan/task/leakage-report/export-manifest contracts, receipt-derived temporal policy, component-level split isolation from required declarations plus exact release relationships, private-held-out/public-split policy, evidence-backed task projection, and database-independent deterministic verification after the existing explicit release-replay gate. This criterion remains unfinished until the exact reviewed head, merged tree, protected Pilot A export, and independently downloaded artifact pass; unsupported-by-evidence task families, Comparator, remaining pilots, and full 1.0 acceptance also remain open.
+Issue [#57](https://github.com/Mnehmos/MathOS/issues/57) completed Phase 6c through PR [#58](https://github.com/Mnehmos/MathOS/pull/58). Reviewed head `2d0c8fd0ec417ea0801d8995d4b93414fcf0a814` merged as `4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`. Exact-head CI `29889101827`, merged-tree CI `29889317590`, and protected publication run `29889317589` passed the closed RL contracts, receipt-derived temporal policy, component-level split isolation, private-held-out/public-split policy, evidence-backed task projection, explicit family skips, and offline deterministic verification after the separate release-replay gate.
+
+Artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078ae80e1a6e7b9ab2b`, is 470,757 archive bytes with GitHub SHA-256 `5598132289fe4a6c7d5527f5dcad4129e2a1048fd3f5ea2a912d72af1902197a`; it expands to 360 files and 885,321 bytes with no links. Protected Lean 4.32 replay and independent offline reprojection bind source release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567`, canonical plan `0fe5bca2a96bff6c924cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, and RL export `fc0d4ccd3945aa3275a670dd5d367881c483c599bfa5350a604ed99a5ef3a5e5`. The exact 31-file export has 30 manifest members, 102,369 member bytes, 10 private held-out tasks, one leakage component, and six emitted families. Every inventory/hash/schema/source/split/temporal/reprojection check passed with a nonexistent instance root; independent audit found zero policy failures, unresolved trust-evidence references, cross-claim variants, cross-split overlaps, or forbidden reasoning fields. Decomposition, proof repair, generalization, frontier selection, Comparator, remaining pilots, migration, and full 1.0 acceptance remain open.
 
 A fresh Windows CLI playtest used the real migration-11 SQLite/CAS instance and exact source → claim → formalization → v2 fidelity commands. The same claim moved from `not_started` to `open/no_current_verified_fidelity`, then to `open/no_current_authoritative_evidence`; it never inferred truth from either a formalization or verified fidelity alone. Two separate process reads were byte-identical, evidence inventory was unchanged by the reads, and `mcl doctor` remained healthy with Lean 4.32.0 visible. The protected merged-tree artifact separately records `open/no_current_verified_fidelity` after formal authority and `proved` only after role-separated verified v2 fidelity.
 
@@ -242,9 +244,9 @@ These items establish only part of the product foundation and trace model. One e
 
 ## Next highest-priority criteria
 
-1. Complete review, protected execution, and independent artifact audit for issue #57's leakage-aware RL/evaluation export without promoting private or held-out evidence.
-2. Define the Comparator package boundary from frozen evid
756A
ence without granting authority.
-3. Continue the remaining pilots and section 30 criteria without treating this partial path as MathOS 1.0.
+1. Define the Comparator package boundary from frozen evidence without granting authority.
+2. Continue the remaining pilots and migration criteria while preserving exact histories and negative attempts.
+3. Complete the remaining section 30 criteria without treating these delivered slices as MathOS 1.0.
 
 ## Exact last validation commands
 
@@ -290,4 +292,4 @@ Observed validation evidence for this update:
 
 ## Release readiness
 
-Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, and corpus-export evidence exist. Phase 6c RL/evaluation implementation is under review and not yet protected/audited; Comparator, remaining pilots, later interfaces, and many section 30 criteria are also unfinished.
+Not ready. Protected Pilot A authority, fidelity, repair, pedagogy, portable-release, corpus-export, and private held-out RL/evaluation evidence exist. Comparator, remaining pilots, migration, later interfaces, and many section 30 criteria are still unfinished.