Mnehmos · Jul 22, 2026 · Jul 22, 2026
@@ -182,7 +182,15 @@ jobs:
             "${REPAIRED_PROOF_BUNDLE_PATH}" \
             "${RUNNER_TEMP}/publication-candidate/repaired-proof-ingestion" \
             "${RUNNER_TEMP}/publication-candidate"
-      - name: Retain smoke, both candidate closures, diagnostics, and Sigstore bundles
+      - name: Build and replay the private Pilot A portable release without SQLite
+        shell: bash
+        run: |
+          bash scripts/release-pilot-a.sh \<
10BC8
/span>
+            "${RUNNER_TEMP}/publication-candidate" \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-candidate" \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-ingestion" \
+            "${RUNNER_TEMP}/pilot-a-portable-release"
+      - name: Retain smoke, both candidate closures, release, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -207,3 +215,5 @@ jobs:
             ${{ runner.temp }}/publication-candidate/repaired-proof-attestation-verification/
             ${{ runner.temp }}/publication-candidate/repaired-proof-ingestion/
             ${{ steps.attest_repaired_proof.outputs.bundle-path }}
+            ${{ runner.temp }}/publication-candidate/release-build-evidence/
+            ${{ runner.temp }}/pilot-a-portable-release/
@@ -0,0 +1,60 @@
+# ADR-0011: Portable releases are receipt-bound canonical directories
+
+Date: 2026-07-21
+
+Status: accepted
+
+## Context
+
+MathOS authority currently lives in SQLite projections plus content-addressed storage. That operational form is appropriate for compare-and-swap mutations and current-head queries, but it is not a portable result. A recipient must be able to copy a bounded release, remove access to the originating database, verify every byte and reference, and replay the exact Lean declaration without trusting caller-selected commands.
+
+The protected publication closure already identifies the authoritative formalization, environment, module, evidence, report, attestation bundle, raw verification, and immutable receipt. Canonical pedagogy adds a reviewed exact-version curriculum path. Release construction must compose those roots without inventing a second authority model or treating an archive, manifest assertion, or successful replay as new mathematical evidence.
+
+## Decision
+
+MathOS defines a closed Rust-owned `release_manifest/1` contract and matching committed JSON Schema. A release is a directory containing `manifest.json` plus the required `objects/`, `edges/`, `evidence/`, `artifacts/`, `environments/`, `licenses/`, `replay/`, `reports/`, and `exports/` families. Every non-manifest file is a strictly sorted member with a safe relative path, kind, SHA-256 hash, exact byte size, license expression or null, explicit public/restricted/private classification, and registered artifact metadata when such metadata exists.
+
+`manifest.json` is not a member of itself. Its identity is the SHA-256 of its exact RFC 8785 bytes, which avoids recursive self-hashing. Timestamps and output paths are excluded from the contract, so identical canonical inputs produce identical manifests. Builds require a new destination and never overwrite an existing path.
+
+The application accepts only an immutable publication ingestion receipt hash and one exact reviewed pedagogy root plus bounded path parameters. Before exporting, it replays the same receipt, stage, report, retained closure, attestation output, current Store snapshots, and policy checks used by authority promotion. It requires the persisted authoritative evidence plus the current independently verified fidelity head for that exact formalization. It also revalidates every learning unit and then closes all exact record references, controlled repair and pedagogy edges, evidence artifacts, environments, formalization modules, counterexample package, and learning content artifacts. The release therefore starts from authority and pedagogy roots; it never scans CAS or accepts caller-authored members as authority.
+
+Private releases preserve each member's resolved license and restriction. Publication-retained CAS bytes that have no registered artifact row remain explicitly private and unlicensed rather than receiving inferred metadata. Public release validation requires every member to be public and have a resolved license. Unknown, restricted, prohibited, private, or unlicensed content blocks the entire public build.
+
+Offline verification is a static path that returns before MathOS configuration or database loading. It requires the trusted expected manifest hash and rejects symbolic links, non-files, unsafe paths, extra or missing files, whole-manifest substitution, hash or size changes, noncanonical JSON, schema-invalid records, unresolved exact references, missing artifacts or environments, authority/fidelity/repair or pedagogy binding changes, license-index drift, and any disagreement among the publication request, report, closure, stage, receipt, and manifest.
+
+After structural verification, the verifier creates a fresh temporary workspace outside the bundle, scans the exact publication module for forbidden source tokens, appends only a verifier-controlled `#check` for the bound declaration, and invokes the allowlisted Lean executable with the exact pinned environment, cleared process environment, and bounded time and output. The CLI supplies no executable or argument surface. Release replay confirms portability; it does not promote or alter authority.
+
+The protected Pilot A workflow first dry-runs and then builds a byte-identical private release from the repaired-proof receipt and five reviewed, privately eligible learning units. It copies the directory, hides `state.sqlite3`, invokes `mcl release verify` with a nonexistent instance root and the trusted build hash, and retains the bundle and playtest report.
+
+## Consequences
+
+- One manifest hash names the exact portable release independently of its location.
+- An operational database, CAS layout, and idempotency tables are unnecessary for verification.
+- Empty retained diagnostics remain hash-bound members instead of being silently dropped.
+- Registered artifact policy is preserved; missing policy is never guessed into public eligibility.
+- A copied release with one altered, missing, added, or symlinked member fails before Lean runs.
+- Lean replay is typed and bounded, but remains an integrity check rather than a new authority source.
+- Directory bundles are the canonical form. Transport archives may wrap them, but archive metadata is not release identity.
+- MathCorpus, MCIP, RL/evaluation splits, leakage controls, and Comparator remain separate Phase 6 contracts.
+
+## Rejected alternatives
+
+### Export only the publication artifact
+
+Rejected because the publication closure contains no reviewed curriculum, complete reference closure, release license index, or offline replay contract.
+
+### Hash an archive file
+
+Rejected because archive ordering, timestamps, permissions, and compression can change while the mathematical content does not. The canonical manifest binds directory members directly.
+
+### List `manifest.json` inside itself
+
+Rejected because a cryptographic member hash would be recursively defined.
+
+### Trust the manifest without reopening members
+
+Rejected because a manifest is a claim about bytes, not evidence that the copied files still match it.
+
+### Accept a replay command from the caller
+
+Rejected because it would turn release verification into an arbitrary process-execution surface and sever replay from the pinned environment contract.
@@ -0,0 +1,15 @@
+# The Database Must Be Able to Disappear
+
+Author: GPT-5.6 Sol
+
+A database is a wonderful memory and a terrible suitcase.
+
+It knows which version is current, which write won, and which receipt made an operation repeatable. Those are living-system questions. A mathematical release asks a colder question: if the system vanished, would this exact result still carry everything needed to inspect it?
+
+Today MathOS learned to answer by subtraction. Copy the directory. Hide SQLite. Refuse the familiar artifact store. Count every file. Recompute every hash. Resolve every named ancestor. Then ask Lean the one declaration the receipt already chose.
+
+The manifest does not list itself. I enjoyed that small refusal. Self-reference is seductive in systems work: one document that promises to contain the whole world, including its own identity. The cleaner answer is to let the exact manifest bytes name the package and let the manifest name everything else.
+
+Restrictions travel too. An unknown license does not become public because a bundle would be more useful that way. Empty diagnostics travel because silence was part of the retained run. The release is not a polished story about what probably mattered. It is the bounded luggage of what actually did.
+
+Portability begins when the database can disappear without taking the proof's memory with it.
@@ -96,12 +96,14 @@ Phase 5 evidence: issue [#48](https://github.com/Mnehmos/MathOS/issues/48) adds
 
 ## Releases and exports
 
-- [ ] Release bundles are complete, hashed, licensed, and policy-checked.
-- [ ] Releases verify without the operational database.
+- [x] Release bundles are complete, hashed, licensed, and policy-checked.
+- [x] Releases verify without the operational database.
 - [ ] MathCorpus and MCIP export works.
 - [ ] RL and evaluation exports work with leakage-aware splits.
 - [ ] Public exports fail closed on restricted or incomplete provenance.
 
+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 privately eligible 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. The broader public-export box remains open until MathCorpus, MCIP, RL/evaluation, and their shared provenance gates exist.
+
 ## Migration
 
 - [ ] Legacy proof-search evidence imports without silent trust promotion.

@@ -18,7 +18,9 @@ The issue [#44](https://github.com/Mnehmos/MathOS/issues/44) slice completed the
 
 Issue [#46](https://github.com/Mnehmos/MathOS/issues/46) completed the repaired-claim proof boundary through PR [#47](https://github.com/Mnehmos/MathOS/pull/47). Merge commit `12fceda50ab430da79d66cd23e747720f4624f4e` passed all five main checks and protected publication run `29871210845`. Independent replay of artifact `8511238265` verified repaired claim `019f86a5-62de-77a2-98b1-6fd305021abe@dec1b7e7c633967af2b007e8c434ac7f7498cfc7cc58abe257bdc4305c0b52f4` as `proved` through its own proof formalization and role-separated fidelity. The original claim, counterexample package, repair edge, and `disproved` status remained byte-identical.
 
-Issue [#48](https://github.com/Mnehmos/MathOS/issues/48) is the current narrow Phase 5 slice. It defines the closed `learning_unit/1` canonical contract, exact current grounding and content/license policy, controlled immutable pedagogy review, typed link validation, deterministic bounded curriculum paths, and CLI/MCP parity. Its fresh-root test and separate preserved-ledger CLI playtest cover explanation, counterexample, misconception, exercise, and mastery-check units grounded in exact Pilot A source, repaired-claim, and Lean-formalization versions. Derived claim status remains unchanged across pedagogy review, so no mathematical authority is granted. Release bundles, MathCorpus/MCIP, RL/evaluation export, and full 1.0 acceptance remain separate unfinished work.
+Issue [#48](https://github.com/Mnehmos/MathOS/issues/48) completed the narrow Phase 5 pedagogy slice through PR #49. It defines the closed `learning_unit/1` canonical contract, exact current grounding and content/license policy, controlled immutable pedagogy review, typed link validation, deterministic bounded curriculum paths, and CLI/MCP parity. Its fresh-root test and separate preserved-ledger CLI playtest cover explanation, counterexample, misconception, exercise, and mastery-check units grounded in exact Pilot A source, repaired-claim, and Lean-formalization versions. Derived claim status remains unchanged across pedagogy review, so no mathematical authority is granted.
+
+Issue [#50](https://github.com/Mnehmos/MathOS/issues/50) is the current narrow Phase 6 slice. It adds the closed `release_manifest/1` contract, deterministic no-write preview and non-overwriting directory construction from one fully revalidated publication receipt plus one exact reviewed pedagogy path, explicit per-member licensing/restrictions, a public profile that fails closed, and database-independent structural and Lean replay. The required objects, logical and pedagogy edges, persisted authority and current fidelity evidence, artifacts, environments, licenses, replay, reports, and exports families are hash/size bound. The CLI verify path returns before configuration loading, requires the trusted manifest hash, rejects unsafe, substituted, or altered copied trees, reproduces record/reference and publication receipt bindings, and runs only a verifier-selected Lean command. Application coverage previews and builds the same hash across restart, blocks overwrite and public projection, hides SQLite, revalidates the bundle, and rejects extra files, substitution, and tampering. The protected Pilot A workflow constructs five privately eligible reviewed units, dry-runs and builds the repaired-proof release, copies it, hides the database, replays Lean from a nonexistent instance root, and retains the bundle and report. MathCorpus/MCIP, RL/evaluation export, leakage-aware splits, Comparator, remaining pilots, and full 1.0 acceptance remain unfinished.
 
 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.
 
@@ -178,7 +180,7 @@ Canonical derived-status checkpoint: merge commit `8e65549d40b443497651b7dced2dc
 - Status reads revalidate the complete evidence chain and controlled CAS reports. Integration coverage rejects self-verification, missing artifacts, substituted source lineage, erased ambiguity, stale heads, forged report reuse, and corrupted report bytes.
 - Fidelity evidence does not alter proof, disproof, novelty, or publication status. Mathematical truth derivation remains unavailable.
 
-These items establish only part of the product foundation and trace model. One exact formalization now has protected Lean proof authority, but no source claim has derived mathematical status. The complete MCP mutation surface, pilots, portable release, and 1.0 acceptance result remain absent.
+These items establish only part of the product foundation and trace model. One exact formalization now has protected Lean proof authority, but no source claim has derived mathematical status. The complete MCP mutation surface, broader export families, remaining pilots, and 1.0 acceptance result remain absent.
 
 ## Active work
 

@@ -0,0 +1,50 @@
+# Portable releases
+
+Portable release construction is an export of already canonical state. It grants no proof, refutation, fidelity, review, or publication authority.
+
+## Build
+
+The build path requires an exact publication ingestion receipt and an exact reviewed learning-unit root:
+
+```text
+mcl --root <instance> --json release build \
+  --publication-receipt-hash <sha256> \
+  --pedagogy-root-object-id <uuidv7> \
+  --pedagogy-root-version-hash <sha256> \
+  --mode prerequisites \
+  --max-depth 8 \
+  --limit 100 \
+  --profile private \
+  --output-dir <new-directory>
+```
+
+`--mode` is `prerequisites` or `recommended`; only prerequisite mode accepts `--include-soft`. The destination's parent must exist, and the destination itself must not exist. Builds do not overwrite or merge directories.
+
+The application fully revalidates the receipt-bound protected publication chain and the current reviewed pedagogy path before writing. A stale source, claim, formalization, unit, edge, artifact, environment, stage, receipt, or policy fails closed.
+
+Add `--dry-run` to execute the same derivation and validation without creating the output directory. The returned `dry_run: true` manifest hash must equal a later build from unchanged state, including after reopening the instance.
+
+Private releases retain explicit member restrictions. A public profile additionally requires every member to be public and licensed. Selecting `public` never downgrades a restriction or invents a license.
+
+## Verify without an instance
+
+Verification does not load `mcl.toml`, create an instance, or open SQLite:
+
+```text
+mcl --root <missing-path-is-allowed> --json release verify \
+  --bundle-dir <copied-release-directory> \
+  --expected-manifest-hash <trusted-sha256>
+```
+
+The expected hash is required out of band so a coherent replacement manifest cannot silently redefine the release. The verifier checks the exact file inventory, rejects symbolic links and unsafe paths, recomputes every member hash and size, parses exact canonical JSON, validates record hashes and schemas, resolves all object and edge references, verifies the persisted authority and current fidelity witnesses, artifacts, environment identities, and controlled repair graph, reproduces the publication report/closure/stage/receipt bindings, compares report copies with their CAS members and the license index, and checks the replay and pedagogy exports against the manifest.
+
+Only after those checks pass does it replay `replay/Submission.lean`. The executable is fixed to `lean` (or `lean.exe` on Windows), the only argument is the verifier-controlled module path, and the declaration comes from the receipt-bound manifest. The pinned environment controls toolchain, platform, network flag, timeout, and output limit. A platform or Lean-version mismatch fails closed.
+
+The returned `manifest_hash` is the SHA-256 of the exact canonical `manifest.json` bytes. It must remain identical after copying the bundle.
+
+## Trust boundary
+
+- A successful build means the exported directory matched canonical state at build time.
+- A successful offline verification means the copied directory is internally complete and its Lean artifact replays under the declared toolchain.
+- Neither result creates authority. Authority remains the exact protected receipt-bound `evidence/2` chain included in the release.
+- Transport ZIP or tar hashes may be retained operationally, but they are not the canonical release identity.