Mnehmos · Jul 25, 2026 · Jul 25, 2026 · Jul 25, 2026
@@ -8,6 +8,7 @@ scripts/comparator-network-probe.py text eol=lf
 schemas/mathcorpus/upstream-*/* -text
 schemas/mcip/v1/upstream-*/* -text
 fixtures/comparator/authority/* -text
+fixtures/bh_formalization/* text eol=lf
 
 # RL export embeds these schemas as deterministic member bytes on every platform.
 schemas/release/rl-*.schema.json text eol=lf
@@ -0,0 +1,81 @@
+# ADR-0017: Non-null source content is a verified portable binding
+
+Date: 2026-07-25
+
+Status: accepted
+
+## Context
+
+The closed `source/1` schema already permits an optional SHA-256 `content_hash`. Syntax validation
+previously established only that a non-null value looked like a hash. Source create and version
+operations could therefore name missing bytes, an unrelated artifact, generated output, or content
+whose license and redistribution policy contradicted the source record. Portable releases included
+the source record but did not derive an artifact member from that field.
+
+That gap matters before BH Pilot C. A provenance record that survives while its named source bytes
+do not is not a database-independent research source boundary. At the same time, changing
+`source/1` would alter existing canonical 
8000
identities, and treating source availability as fidelity
+or mathematical authority would collapse separate trust roles.
+
+## Decision
+
+`source/1` bytes and hashes remain unchanged. `content_hash: null` continues to mean that exact
+source bytes are unavailable.
+
+When `content_hash` is non-null, the application requires a registered CAS artifact whose bytes
+rehash to that identity. Its immutable metadata must carry the reviewed `source_content` role, use
+user-ingest/import/migration provenance, and be no less restrictive than the source's license,
+redaction, and redistribution declarations. The check runs before create/version dry runs,
+idempotency lookup, and persistence so an idempotent retry cannot conceal later CAS loss.
+
+Migration 0013 adds a separate SQL insert trigger over the relational metadata projections and
+fails closed if existing source versions violate the new closure. It cannot replace CAS
+verification; it prevents direct SQL from bypassing the registered-role and policy contract.
+
+Release construction derives every non-null source hash from the exact record closure, includes its
+bytes and metadata at `artifacts/<sha256>`, and fails if CAS or metadata no longer verifies.
+Database-free release verification enforces exact artifact paths and identities and reruns the same
+source-content policy from manifest-retained metadata.
+
+The initial conformance fixture is the Apache-2.0 `SOURCE-LOCK.md` file from the exact pinned
+`Mnehmos/BHFormalization` commit. It exercises source portability only.
+
+## Consequences
+
+- Existing null source bindings remain compatible and do not invent unavailable bytes.
+- A non-null binding is meaningful across CLI, MCP, retry, restart, direct SQL defense, and copied
+  releases.
+- Public redistribution cannot be inferred from a source record when the exact artifact is private,
+  unlicensed, or differently licensed.
+- An incompatible legacy non-null binding blocks migration until an operator supplies a reviewed
+  exact artifact instead of receiving silent trust promotion.
+- Release verification remains independent of SQLite while retaining the policy inputs it checks.
+- The decision creates no statement fidelity, Lean proof/refutation, Comparator authority, or
+  derived source truth.
+
+## Rejected alternatives
+
+### Keep syntax-only hashes
+
+Rejected because a well-formed digest without retained verified bytes is not a source-content
+closure.
+
+### Embed artifact bytes in `source/2`
+
+Rejected because the CAS and release manifest already provide immutable byte identity and policy,
+while a schema revision would unnecessarily change canonical source hashes.
+
+### Trust any registered artifact
+
+Rejected because generated reports, verifier outputs, and review documents can be registered
+artifacts but are not thereby source content.
+
+### Check only during release construction
+
+Rejected because canonical source state and idempotent retries would remain able to bind missing or
+misclassified content.
+
+### Infer fidelity or authority from exact bytes
+
+Rejected because byte integrity and provenance do not establish that a formalization matches the
+source or that a mathematical claim is true.
@@ -1,6 +1,6 @@
 # MathOS 1.0.0 Release Checklist
 
-Last updated: 2026-07-22
+Last updated: 2026-07-25
 
 This checklist mirrors section 30 of [SPEC.md](../../SPEC.md). A checked item requires linked mechanical and manual evidence. Partial Phase 1 work is recorded below but does not check a release item whose complete wording is not yet satisfied.
 
@@ -118,6 +118,8 @@ Phase 6e Comparator-execution issue [#63](https://github.com/Mnehmos/MathOS/issu
 
 Phase 6f issue [#65](https://github.com/Mnehmos/MathOS/issues/65) completed through PR [#66](https://github.com/Mnehmos/MathOS/pull/66), merge `3e199a847a27202bfdf04db8384ebf930c275325`, tree `940f0f6e2cb0abe1c4bfcace607eab2235ec6414`. Exact-head CI `30172477751`, merged-tree CI `30172614043`, and protected publication `30172614051` passed. Downloaded artifact `8623423197` has Actions digest `sha256:824949af9590d58a3c7e39eaa25edac3d2779b9d3650b984332884b584172a26`; an independent database-free audit checked all 139 files, 91 portable objects, 104 staged artifacts, exact retry bytes, and every authority/provenance/currentness binding with no links or database files. Stage `b4c84618c1266186a58bd69adf161f6234563b98af01dd5d31aab6a43eb8179e` produced receipt `5f4b8c61134728c0e35b653ae17c7a3075f52bbfeff2b6fe7c5435845ae7a0cc` and current authoritative evidence `019f9ae3-4217-7591-897a-fc97d7188a34@349684d71dc51ee1c526c533ae661daee44c09b61419ac441d1474776fd0bfeb`. Report `1fa186aab178215280e63675d36c4be497106db238f70f9cf09489edd2c04233`, package verification `f8587103c57136ede329d8bde4ab268f3ca9e7fb0596d01d40bdb14989637e23`, release manifest `e93c8644f4053645b888f3347c45bc8757ace33660c8fa1b2fea75796eb65beb`, attestation bundle `28a7294ff0aafe89bc0ef75c1d87d7b532d1c4458d6a9caa017c13fd1cc68e12`, and raw verification `81bd23fc9262d36a1a781320e5c8b08e876991459
10BC8
6543d9f278af8b9ae997cf8` replay exactly. Report and receipt stay non-authoritative; Comparator authority remains excluded from Lean proof/refutation claim status.
 
+Phase 6g source-content closure is tracked in issue [#71](https://github.com/Mnehmos/MathOS/issues/71). Non-null `source/1.content_hash` now requires exact verified CAS bytes plus reviewed source-content provenance and compatible license/restriction policy before create, version, dry-run, or retry. Migration 0013 independently rejects direct SQL bypass and invalid legacy bindings. Portable release construction includes those exact bytes and metadata; database-free verification repeats the same semantic policy. Null source hashes remain compatible. The pinned BH source-lock CLI and release fixtures prove byte identity and offline retention but deliberately establish no Pilot C fidelity or mathematical authority.
+
 ## Migration
 
 - [ ] Legacy proof-search evidence imports without silent trust promotion.

@@ -42,6 +42,8 @@ Issue [#65](https://github.com/Mnehmos/MathOS/issues/65) completed the Phase 6f
 
 Downloaded artifact `8623423197`, `comparator-run-3e199a847a27202bfdf04db8384ebf930c275325`, has Actions archive digest `sha256:824949af9590d58a3c7e39eaa25edac3d2779b9d3650b984332884b584172a26`. Independent database-free audit checked all 139 files, 91 portable CAS objects, 104 staged artifacts, the exact 20-file run and 84-file release, zero links/reparse points, zero database files, canonical bytes, retry stability, and every retained binding. Stage `b4c84618c1266186a58bd69adf161f6234563b98af01dd5d31aab6a43eb8179e` produced receipt `5f4b8c61134728c0e35b653ae17c7a3075f52bbfeff2b6fe7c5435845ae7a0cc` and authoritative Comparator evidence `019f9ae3-4217-7591-897a-fc97d7188a34@349684d71dc51ee1c526c533ae661daee44c09b61419ac441d1474776fd0bfeb`. Live replay is `current` and `authoritative: true`; its exact report `1fa186aab178215280e63675d36c4be497106db238f70f9cf09489edd2c04233`, package verification `f8587103c57136ede329d8bde4ab268f3ca9e7fb0596d01d40bdb14989637e23`, release manifest `e93c8644f4053645b888f3347c45bc8757ace33660c8fa1b2fea75796eb65beb`, attestation bundle `28a7294ff0aafe89bc0ef75c1d87d7b532d1c4458d6a9caa017c13fd1cc68e12`, and raw verification `81bd23fc9262d36a1a781320e5c8b08e8769914596543d9f278af8b9ae997cf8` all replay exactly. The report and receipt remain structurally non-authoritative, and Comparator evidence remains excluded from proof/refutation claim-status inputs. The exact protected probe is now LF-pinned across Windows checkouts because its digest is part of the invocation binding.
 
+Issue [#71](https://github.com/Mnehmos/MathOS/issues/71) is the focused Phase 6g boundary before BH Pilot C. It keeps `source/1` canonical bytes unchanged and closes non-null `content_hash` across mutation, retry, restart, direct SQL defense, migration, portable release construction, and database-free verification. Exact source artifacts require the reviewed `source_content` role, user-ingest/import/migration provenance, and compatible license/restriction policy. The pinned Apache-2.0 `Mnehmos/BHFormalization` source-lock fixture exercises the boundary without importing the paper or either certificate and without creating fidelity, Lean-kernel, Comparator, or mathematical-status authority.
+
 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.

@@ -38,6 +38,16 @@ mcl artifact verify --artifact-hash <sha256>
 
 Verification rereads the bytes from CAS, recomputes their hash, validates their media representation, and compares their size with canonical metadata. It establishes storage integrity only.
 
+## Source-content gate
+
+A non-null `source/1.content_hash` is accepted only after the exact CAS bytes verify and immutable
+metadata carries the reviewed `source_content` role with compatible provenance, license, and
+restriction. Null remains the explicit representation for source records without retained exact
+bytes. Portable releases carry and revalidate every non-null source artifact without SQLite.
+
+The complete contract is documented in [Exact source content](SOURCES.md) and
+[ADR-0017](../decisions/ADR-0017-source-content-is-a-verified-portable-binding.md).
+
 ## Formalization gate
 
 A formalization may name a module artifact only when that exact hash is registered with media type `text/x-lean`. A missing artifact and an artifact of another media type both fail before the formalization becomes canonical state.

@@ -20,7 +20,7 @@ mcl --root <instance> --json release build \
 
 `--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.
+The application fully revalidates the receipt-bound protected publication chain and the current reviewed pedagogy path before writing. Every non-null `source/1.content_hash` in that exact object closure contributes its verified CAS bytes and retained metadata to the artifact inventory. 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.
 
@@ -36,7 +36,7 @@ mcl --root <missing-path-is-allowed> --json release verify \
   --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.
+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, requires exact path and retained policy metadata for non-null source content, 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.
 

@@ -0,0 +1,65 @@
+# Exact source content
+
+A canonical `source/1` record describes provenance and may optionally bind exact retained bytes
+through `content_hash`. That hash is an integrity and portability reference only. It does not prove
+that the bytes are faithful to a paper, correct, complete, or mathematically authoritative.
+
+## Null and non-null bindings
+
+`content_hash: null` remains valid. It means MathOS has provenance text but no exact source-content
+artifact to verify or carry into a release.
+
+A non-null `content_hash` must resolve to the exact SHA-256 bytes in the local content-addressed
+store. The registered immutable `artifact_metadata/1` must satisfy all of these conditions:
+
+- `semantic_metadata.source_role` is exactly `source_content`;
+- `creation_source` is `user_ingest`, `import`, or `migration`, never generated, verifier-produced,
+  or human-review output;
+- a source license, when present, exactly matches the artifact license; and
+- a public source with allowed redistribution has a public artifact and the same resolved license.
+
+The application re-reads and hashes the CAS bytes before every source create or version proposal,
+including dry runs and idempotent retries. A missing, changed, unregistered, wrongly classified, or
+policy-incompatible artifact returns `MCL_SOURCE_CONTENT_INVALID` before state changes.
+
+The `original_text` field remains canonical source context; it is not silently treated as the
+artifact bytes. Callers that need byte identity must use the non-null `content_hash`.
+
+## Store defense and migration
+
+Migration `0013_source_content_closure.sql` independently rejects direct `record_versions` inserts
+whose non-null source hash does not resolve to compatible immutable artifact metadata. It also
+checks every existing source version while upgrading. An incompatible legacy binding blocks the
+migration instead of being silently promoted to reviewed source content.
+
+SQLite cannot prove that the CAS file still exists or matches its name. The application performs
+that byte check before mutation, and portable release construction repeats it while materializing
+the closure.
+
+## Portable releases
+
+Release construction adds every non-null source content hash in the exact object-reference closure
+to `artifacts/<sha256>`. The manifest retains its artifact metadata and policy. Database-free
+verification requires the exact artifact path and hash, requires retained metadata, and reruns the
+same role, provenance, license, and redistribution policy checks.
+
+Removing the operational database therefore does not remove the source bytes or the evidence
+needed to decide whether they were eligible for the release. A source with `content_hash: null`
+adds no invented artifact member.
+
+## BH Pilot C fixture
+
+`fixtures/bh_formalization/SOURCE-LOCK.md` is copied byte-for-byte from
+`Mnehmos/BHFormalization` commit `8875bef812375d7e6fd00bff95764cd5c057c7fe`, tree
+`600f3e1230ca88f9784837933e2417c319aaad3e`. The GitHub content object is blob
+`c7e3805ab78327f1cd561421e2c0168a009eb161` with 1,809 bytes. Its SHA-256 is
+`249f62a4e2780235239cf9f4e781f274f8dadba7f3aeba3aab51f46b0a6fc5c5`.
+The earlier
+`c82096766a9df350fc2584cdabd0e18334348a1a8adbd4fc7ec24d75ff2994ee`
+discovery digest was a CRLF Windows worktree rendering, not the pinned Git object, and is
+deliberately not used as the portable identity.
+The adjacent Apache-2.0 `LICENSE` and `NOTICE` preserve upstream terms and attribution.
+
+This fixture tests exact source ingestion and database-independent release closure. It is not the
+BH paper, the paper's reproducibility certificate, or a fidelity, Lean-kernel, Comparator, or
+mathematical-status witness.