Mnehmos · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026
@@ -4,3 +4,6 @@
 # These vendored files are cryptographic inputs and must retain their upstream bytes.
 schemas/mathcorpus/upstream-*/* -text
 schemas/mcip/v1/upstream-*/* -text
+
+# RL export embeds these schemas as deterministic member bytes on every platform.
+schemas/release/rl-*.schema.json text eol=lf
@@ -182,16 +182,17 @@ jobs:
             "${REPAIRED_PROOF_BUNDLE_PATH}" \
             "${RUNNER_TEMP}/publication-candidate/repaired-proof-ingestion" \
             "${RUNNER_TEMP}/publication-candidate"
-      - name: Build, replay, and corpus-export private Pilot A without SQLite
+      - name: Build, replay, and export private Pilot A without SQLite
         shell: bash
         run: |
           bash scripts/release-pilot-a.sh \
             "${RUNNER_TEMP}/publication-candidate" \
             "${RUNNER_TEMP}/publication-candidate/repaired-proof-candidate" \
             "${RUNNER_TEMP}/publication-candidate/repaired-proof-ingestion" \
             "${RUNNER_TEMP}/pilot-a-portable-release" \
-            "${RUNNER_TEMP}/pilot-a-mathcorpus-mcip-export"
-      - name: Retain smoke, candidate closures, release, corpus export, diagnostics, and Sigstore bundles
+            "${RUNNER_TEMP}/pilot-a-mathcorpus-mcip-export" \
+            "${RUNNER_TEMP}/pilot-a-rl-evaluation-export"
+      - name: Retain smoke, candidate closures, release, exports, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -219,3 +220,4 @@ jobs:
             ${{ runner.temp }}/publication-candidate/release-build-evidence/
             ${{ runner.temp }}/pilot-a-portable-release/
             ${{ runner.temp }}/pilot-a-mathcorpus-mcip-export/
+            ${{ runner.temp }}/pilot-a-rl-evaluation-export/
@@ -38,6 +38,7 @@ See:
 - [Real blockers](docs/implementation/BLOCKERS.md)
 - [Release checklist](docs/implementation/RELEASE_CHECKLIST.md)
 - [MathCorpus and MCIP export](docs/implementation/CORPUS_EXPORT.md)
+- [RL and evaluation export](docs/implementation/RL_EVALUATION_EXPORT.md)
 - [Architecture decisions](docs/decisions/)
 
 The implementation agent must continue until the complete specification passes. A pilot, demo, schema, or partially working command is not completion.

@@ -0,0 +1,81 @@
+# ADR-0013: RL and evaluation splits are component-locked frozen-release projections
+
+Date: 2026-07-22
+
+Status: accepted
+
+## Context
+
+Row-random dataset splitting can put a theorem, an equivalent statement, its source paper, a
+certificate sibling, or a proof variant on both sides of an evaluation boundary. A frozen
+MathOS release contains exact evidence for some of those relationships, but semantic
+equivalence, generated families, benchmark identity, and publication chronology cannot all be
+reliably inferred from proof text.
+
+RL data is also derived data. It must not become canonical state, turn diagnostic traces into
+proof, weaken release licensing, or make a private release public or trainable.
+
+## Decision
+
+MathOS accepts a closed `rl_export_plan/1` cohort plan. Every named source release is bound by
+its expected manifest SHA-256, one of `train`, `validation`, `public_test`, or
+`held_out_evaluation`, a benchmark identity, and explicit nonempty labels for theorem-dependency,
+equivalent-formalization, shared-source, certificate-family, and proof-variant relationships.
+The signed publication receipt, not caller text, supplies the exact publication date.
+
+The exporter first structurally verifies every release. The protected producer separately runs
+the release's platform-bound Lean replay immediately before projection while SQLite is hidden.
+The exporter then adds derived keys for shared exact records, source locators and content,
+claim/formalization identity, normalized nonempty import manifests, proof modules and
+declarations, typed dependency/equivalence/repair edges, and counterexample run/package lineage.
+Any releases sharing a declared or derived key are unioned into one leakage component. Every
+component must have exactly one split. Training dates must be at or before the plan cutoff;
+validation, public test, and held-out dates must be later.
+
+Private releases are permitted only in `held_out_evaluation`. Train, validation, and public test
+therefore require a release that already passed the complete public-release member and license
+policy. Task and evidence members retain explicit licenses and restrictions.
+
+`mcl release export-rl` emits only tasks backed by exact current fidelity plus receipt-bound
+kernel authority. Version 1 projects formalization, fidelity selection, counterexample, statement
+repair, declaration retrieval, and proof generation. Reviewed split-eligible pedagogy can also
+produce explanation and curriculum-ordering tasks. All twelve SPEC task families appear in the
+family audit; missing evidence and the four not-yet-projected families have explicit skip reasons.
+Private chain-of-thought fields are rejected and never treated as proof evidence.
+
+`mcl release verify-rl-export` requires the trusted export-manifest hash, an independent plan, and
+the named frozen releases. It revalidates their closed semantic inventories, recomputes the
+complete projection, and requires byte-identical output without SQLite or network access. Lean
+replay remains the preceding platform-bound `mcl release verify` gate, not a hidden portability
+requirement of the derived export.
+
+## Consequences
+
+- A row cannot be moved independently of its dependency/equivalence/source/certificate/proof/
+  benchmark component.
+- Caller-declared relations supplement exact derived identities but cannot replace them.
+- Publication chronology is receipt-bound and mechanically enforced.
+- Private Pilot A can exercise the evaluation path without becoming training data.
+- The export is portable derived evidence; the canonical store and frozen releases remain truth.
+- Decomposition, proof repair, generalization, and frontier selection remain explicit future
+  projections until their required source evidence exists.
+
+## Rejected alternatives
+
+### Random or task-ID-based splitting
+
+Rejected because cryptographically distinct rows can still disclose the same mathematics.
+
+### Infer every relation from theorem text
+
+Rejected because semantic equivalence, benchmark membership, and certificate family are review
+decisions, not reliable string properties.
+
+### Allow private training with a plan flag
+
+Rejected because a split label cannot manufacture redistribution, redaction, or training rights.
+
+### Verify only internal export hashes
+
+Rejected because a coherent substituted export can redefine its own manifest. Verification also
+requires a trusted hash and exact offline reprojection from independently supplied sources.
@@ -106,6 +106,8 @@ Phase 6 portable-release evidence: issue [#50](https://github.com/Mnehmos/MathOS
 
 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 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.
+
 ## Migration
 
 - [ ] Legacy proof-search evidence imports without silent trust promotion.

@@ -0,0 +1,108 @@
+# RL and evaluation export
+
+`mcl release export-rl` creates a deterministic task dataset from one or more frozen MathOS
+releases. It never opens the operational SQLite database or contacts a network service. The
+split and trust decision is defined by
+[ADR-0013](../decisions/ADR-0013-component-locked-rl-evaluation-projection.md).
+
+## Cohort plan
+
+The plan uses `rl_export_plan/1`. Releases must be sorted by `release_id`, live directly beneath
+the supplied source root, and bind their expected `release_manifest/1` hash. Every leakage label
+array is mandatory, sorted, unique, and nonempty.
+
+```json
+{
+  "schema_version": "rl_export_plan/1",
+  "publication_cutoff": "2026-07-21",
+  "releases": [{
+    "release_id": "pilot-a-release",
+    "expected_manifest_hash": "<sha256>",
+    "split": "held_out_evaluation",
+    "published_on": "2026-07-22",
+    "benchmark_identity": "mathos-pilot-a-prime-parity",
+    "leakage_labels": {
+      "theorem_dependency_components": ["pilot-a-prime-parity"],
+      "equivalent_formalizations": ["pilot-a-refutation-repair"],
+      "shared_sources": ["pilot-a-protected-source"],
+      "certificate_families": ["pilot-a-certificate-family"],
+      "proof_variants": ["pilot-a-proof-family"]
+    }
+  }]
+}
+```
+
+The `published_on` value must equal the UTC date in the release's signed publication receipt.
+Train releases must be dated on or before the cutoff. Validation, public-test, and held-out
+releases must be later. A private release may only be held out.
+
+## Build and verify
+
+```text
+mcl --root does-not-need-to-exist --json release export-rl \
+  --plan /path/to/plan.json \
+  --source-root /path/to/releases \
+  --output-dir /new/path/rl-export \
+  --dry-run
+```
+
+Dry run verifies every source's exact inventory, canonical schemas, references, and receipt-bound
+semantics, resolves every task and output byte, and writes nothing. Remove `--dry-run` to
+atomically create the new directory. Existing destinations are never overwritten. The protected
+producer runs the separate platform-bound `mcl release verify` Lean replay immediately before
+projection; derived export verification remains portable across workers.
+
+Verification needs the trusted output hash plus independent copies of both policy and sources:
+
+```text
+mcl --root does-not-need-to-exist --json release verify-rl-export \
+  --export-dir /path/to/copied-rl-export \
+  --expected-manifest-hash <rl-export-manifest-sha256> \
+  --plan /path/to/plan.json \
+  --source-root /path/to/copied-releases
+```
+
+Verification checks the closed inventory, paths and regular files, canonical JSON, hashes,
+committed schemas, task identities, evidence references, license/restriction policy, receipt
+dates, component isolation, and family audit. It then structurally reverifies all releases and
+byte-compares a fresh deterministic reprojection. It does not silently rerun a source release's
+platform-bound Lean replay under a different verifier environment.
+
+## Output contracts
+
+The root `manifest.json` is `rl_export_manifest/1`. It binds the plan hash, publication cutoff,
+source release/profile/split/component identities, leakage report hash, counts, and every member
+path/hash/size/license/restriction. The manifest itself is excluded from its member inventory to
+avoid recursive identity.
+
+Members include:
+
+- the canonical copied plan and `rl_leakage_report/1`;
+- one canonical `rl_task/1` file per task;
+- the exact source manifest and task-referenced records, evidence, edges, environments, and
+  content-addressed artifacts;
+- the four committed RL schemas.
+
+Task IDs hash every field except the ID itself. Evidence paths and hashes are exact. Trust binds
+the source release, publication receipt, accepted authority evidence, and reviewed fidelity
+evidence. Input and target objects reject `chain_of_thought`, `private_chain_of_thought`, and
+`reasoning_trace` fields.
+
+## Leakage components
+
+MathOS hashes declared labels by dimension and adds exact derived keys, including normalized
+nonempty import manifests. Sharing any key joins releases transitively. A component crossing
+split assignments is rejected; tasks are never reassigned row-by-row. The report lists every
+component, release, split, leakage key, and task ID, with zero accepted cross-split overlap.
+
+## Task families and current limits
+
+Version 1 emits six families when current reviewed fidelity and authoritative kernel evidence are
+present: formalization, fidelity selection, counterexample, statement repair, declaration
+retrieval, and proof generation. Reviewed learning units with a split-compatible training status
+can additionally emit explanation and curriculum ordering.
+
+Decomposition, proof repair, generalization, and frontier selection remain unimplemented
+projections. Any family with no emitted record has a machine-readable skip reason; absence is
+never silently represented as success. Comparator packages, remaining pilots, and full 1.0
+acceptance are separate unfinished work.
diff --git a/docs/implementation/STATUS.md b/docs/implementation/STATUS.md
@@ -26,6 +26,8 @@ Issue [#54](https://github.com/Mnehmos/MathOS/issues/54) completed the focused P
 
 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.
 
+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.
+
 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.
 
 Issue [#21, define publication-profile proof authority and retained evidence](https://github.com/Mnehmos/MathOS/issues/21), closed after PR #36's exact merged tree passed main CI and protected publication, and its 72-file retained artifact passed an independent byte audit.
@@ -240,7 +242,7 @@ These items establish only part of the product foundation and trace model. One e
 
 ## Next highest-priority criteria
 
-1. Implement leakage-aware RL/evaluation splits without promoting private, quarantined, benchmark, or held-out evidence.
+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 evidence without granting authority.
 3. Continue the remaining pilots and section 30 criteria without treating this partial path as MathOS 1.0.
 
@@ -288,4 +290,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, but leakage-aware RL/evaluation exports, Comparator, remaining pilots, later interfaces, and many section 30 criteria are still unfinished.
+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.