Mnehmos · Jul 22, 2026 · Jul 22, 2026 · Jul 22, 2026
@@ -191,8 +191,9 @@ jobs:
             "${RUNNER_TEMP}/publication-candidate/repaired-proof-ingestion" \
             "${RUNNER_TEMP}/pilot-a-portable-release" \
             "${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
+            "${RUNNER_TEMP}/pilot-a-rl-evaluation-export" \
+            "${RUNNER_TEMP}/pilot-a-comparator-package"
+      - name: Retain smoke, candidate closures, release, exports, Comparator package, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -221,3 +222,4 @@ jobs:
             ${{ runner.temp }}/pilot-a-portable-release/
             ${{ runner.temp }}/pilot-a-mathcorpus-mcip-export/
             ${{ runner.temp }}/pilot-a-rl-evaluation-export/
+            ${{ runner.temp }}/pilot-a-comparator-package/
@@ -0,0 +1,89 @@
+# ADR-0014: Comparator-ready packages are deterministic non-authoritative projections
+
+Date: 2026-07-22
+
+Status: accepted
+
+## Context
+
+Comparator protects a different boundary from MathOS publication replay. It compares declarations
+from a trusted challenge environment with a solution, enforces an explicit axiom allowlist, and
+replays the solution through the Lean kernel. Its security argument also depends on a real Linux
+sandbox, exact tool builds, and avoiding prior compilation of potentially adversarial solution
+code.
+
+A five-file package must therefore be portable before it can be verified, but package integrity is
+not Comparator verification. Allowing `verification.json`, a local build, fake-landrun, or an
+ordinary program exit code to claim success would collapse the distinction between prepared input
+and protected verifier evidence.
+
+## Decision
+
+MathOS accepts one closed canonical `comparator_package_plan/1`. The plan binds an exact portable
+release manifest and its headline formalization, contains explicit reviewer-controlled
+`Challenge.lean` source, selects exactly the release declaration, fixes the permitted axioms and
+nanoda setting, records bounded formalization metadata, and pins the fixed Comparator,
+lean4export, and landrun repositories to full commits.
+
+`Solution.lean` is never supplied by the plan. It is copied byte-for-byte from the verified frozen
+release's `replay/Submission.lean` and must match the publication module artifact. The selected
+formalization record, environment/dependency manifest, replay declaration, theorem source, and
+publication binding must all identify that same exact theorem.
+
+The projection contains exactly:
+
+```text
+Challenge.lean
+Solution.lean
+config.json
+formalization.yaml
+verification.json
+```
+
+`config.json` uses the official Comparator module, theorem, axiom, and nanoda fields.
+`formalization.yaml` is deterministic UTF-8 YAML with the frozen identities, reviewed metadata,
+and exact repository/commit pins. The closed `comparator_package_verification/1` record binds the
+four other files, the source-release members, plan hash, and an input fingerprint covering every
+SPEC staleness input.
+
+The verification record has one possible status in this contract: `ready`. Both
+`comparator_verified` and `authoritative` are constant `false`. Construction and offline
+verification create no evidence record and cannot affect claim research status.
+
+`mcl release verify-comparator-package` requires an independently trusted verification hash, the
+canonical plan, the independently supplied frozen release, and its trusted manifest hash. It
+rejects links, reparse points, missing or extra members, noncanonical JSON, altered bytes, changed
+bindings, and any failure of byte-identical deterministic reprojection. It does not open SQLite,
+use the network, or execute Comparator.
+
+## Consequences
+
+- A challenge, solution, theorem source, dependency manifest, configuration, formalization
+  record, plan, or tool-pin change produces a different input fingerprint and package identity.
+- A caller can prepare a challenge but cannot assert that it matches the solution.
+- The package can move independently of the operational database while retaining exact source
+  lineage.
+- Real sandboxed Comparator execution and evidence ingestion remain a separate protected trust
+  transition.
+- Ordinary Lean elaboration of the two package files is only a readiness diagnostic.
+
+## Rejected alternatives
+
+### Copy the solved module as both challenge and solution
+
+Rejected because it does not preserve the independent trusted-challenge boundary and weakens the
+meaning of statement comparison.
+
+### Generate a challenge by rewriting arbitrary Lean proof text
+
+Rejected because a text rewrite is not a Lean parser and could silently alter scope, declarations,
+macros, or the theorem statement.
+
+### Store `Comparator-verified` in the package plan
+
+Rejected because caller-authored metadata and package construction are not verifier evidence.
+
+### Run fake-landrun on Windows and retain the result as publication evidence
+
+Rejected because the official Comparator security assumptions require the real production sandbox;
+fake-landrun is a development aid only.
@@ -110,6 +110,8 @@ Phase 6c leakage-aware RL/evaluation evidence: issue [#57](https://github.com/Mn
 
 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 `0fe5bca2a96bff6c9
8000
24cf837fa91a86b2714cf754c42cf459424f0f1d77ee9e8`, 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.
 
+Phase 6d Comparator-package work is active in issue [#60](https://github.com/Mnehmos/MathOS/issues/60). The closed plan and verification contracts project exactly the five SPEC 20.3 files, copy `Solution.lean` only from a verified frozen release, bind every staleness input and fixed repository/full-commit tool pin, and support trusted-hash offline reprojection. The local Pilot A package reprojected as `ec36212e00e255de770109a44e5bdce2e0e4922491f1a5ae950f93e6ad50ecae` from a nonexistent instance root. It is only `ready`; both verification and authority flags are structurally false. No Comparator or full verification criterion is checked until the real protected Linux sandbox runs and its exact evidence is independently audited.
+
 ## Migration
 
 - [ ] Legacy proof-search evidence imports without silent trust promotion.

@@ -30,6 +30,8 @@ Issue [#57](https://github.com/Mnehmos/MathOS/issues/57) completed Phase 6c thro
 
 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.
 
+Issue [#60](https://github.com/Mnehmos/MathOS/issues/60) is the active Phase 6d slice. It defines closed `comparator_package_plan/1` and `comparator_package_verification/1` contracts and projects the exact SPEC 20.3 five-file package from a frozen release. The plan supplies reviewed challenge source; `Solution.lean` is copied only from the release replay member. Release/formalization/environment/module/declaration, file, plan, input-fingerprint, and fixed repository/full-commit tool bindings are checked offline. The only encodable state is `ready` with `comparator_verified: false` and `authoritative: false`; real sandboxed Comparator execution and evidence remain a later protected transition. A Windows CLI playtest against downloaded protected release `47c72887ebb5421c021c1ed71212e4b4d298f8c02e3d4623223721c2a858f567` produced and independently reprojected five-file package verification `ec36212e00e255de770109a44e5bdce2e0e4922491f1a5ae950f93e6ad50ecae` from a nonexistent instance root. Both Lean files elaborated; the challenge emitted only its intentional `sorry` warning. Exact-head and protected evidence are still required before issue closure.
+
 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
8BD0
_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.
@@ -244,9 +246,9 @@ These items establish only part of the product foundation and trace model. One e
 
 ## Next highest-priority criteria
 
-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.
+1. Complete #60 review, exact-head CI, and protected artifact audit without upgrading `ready` to Comparator verification.
+2. Implement the real Linux-sandboxed Comparator run and controlled evidence transition, then continue the BH Pilot C lifecycle.
+3. Continue remaining pilots, migration, and section 30 criteria while preserving exact histories and negative attempts.
 
 ## Exact last validation commands
 
@@ -266,7 +268,7 @@ git diff --check
 Observed validation evidence for this update:
 
 - Home workstation: Windows 10.0.19045, PowerShell 5.1.19041.6456, Rust 1.97.1, Python 3.12.10, GitHub CLI 2.70.0, GNU Bash 5.2.37 through Git for Windows, and Lean 4.32.0 `x86_64-w64-windows-gnu`.
-- Formatting, warnings-denied Clippy across all targets and features, 156 library tests, 17 CLI tests, four MCP tests, the opt-in real Lean 4.32 lifecycle, all 39 legacy Python regressions, Bash syntax for the modified Pilot A release script, Actionlint 1.7.12, and patch whitespace validation pass for the corpus-export candidate.
+- Formatting, warnings-denied Clippy across all targets and features, 176 library tests, 19 CLI tests, four MCP tests, the opt-in real Lean 4.32 lifecycle, all 39 legacy Python regressions, Bash syntax for the modified Pilot A release script, Actionlint 1.7.12, and patch whitespace validation pass for the Comparator-package candidate.
 - The retained Pilot A release projected twice to manifest `33e6ccc24979e85c14688d755130ace9960f0e074342695e951ac9756c2c590b` with 11 members and 101,695 bytes. Verification from a nonexistent instance root independently reprojected the exact source release and passed every inventory, hash, schema, policy, and binding check. The pinned upstream `validate_packets.py --check-hashes --warn-as-error` and `validate_mcip.py --check-hashes` commands reported zero errors and zero warnings.
 - The application-level authority fixture constructs the real source/claim/formalization, diagnostic and audit jobs/evidence, exact 25-role retained closure, parser-valid protected attestation output, stage, and receipt without fidelity evidence. Dry-run writes no evidence; persisted promotion creates the expected receipt-bound authoritative `evidence/2`; exact retry is identical; and missing staged CAS fails closed. A hands-on Windows CLI smoke applied migration 11, reported healthy `mcl health` and `mcl doctor`, exposed only the receipt-hash promotion surface, and rejected an unknown receipt as `MCL_PUBLICATION_RECEIPT_NOT_FOUND`.
 - CodeRabbit's final review found one uncovered fail-closed test family. Commit `761171fb093cecc4b2391ac53ef89c315ff1eeea` now tests rejected/failed classifications, each required protected-report control independently set false while classification remains passed, and a pre-authoritative report. Formatting, full Rust tests, warnings-denied Clippy, and all five required PR jobs passed on that exact head.

@@ -0,0 +1,56 @@
+# Comparator-ready packages
+
+Comparator package construction is an offline projection of one already verified portable release.
+It prepares inputs; it does not run Comparator or grant authority.
+
+## Build
+
+Create a canonical `comparator_package_plan/1` and supply the frozen release plus its separately
+trusted manifest hash:
+
+```text
+mcl --root <missing-path-is-allowed> --json release export-comparator \
+  --plan <canonical-plan.json> \
+  --bundle-dir <portable-release> \
+  --expected-release-manifest-hash <trusted-release-sha256> \
+  --output-dir <new-package-directory>
+```
+
+Add `--dry-run` to derive the same identity without writing the destination. The destination must
+not exist. The output inventory is exactly `Challenge.lean`, `Solution.lean`, `config.json`,
+`formalization.yaml`, and `verification.json`.
+
+The plan owns the reviewed challenge, theorem name, allowed axioms, nanoda choice, descriptive
+formalization metadata, and full upstream tool pins. `Solution.lean` always comes from the frozen
+release; callers cannot replace it. Version 1 packages exactly the release's headline
+formalization and one theorem.
+
+## Verify without an instance
+
+```text
+mcl --root <missing-path-is-allowed> --json release verify-comparator-package \
+  --package-dir <copied-package> \
+  --expected-verification-hash <trusted-verification-json-sha256> \
+  --plan <canonical-plan.json> \
+  --bundle-dir <portable-release> \
+  --expected-release-manifest-hash <trusted-release-sha256>
+```
+
+Verification checks the exact five-file tree, rejects links and reparse points, recomputes every
+binding, revalidates the source release and exact formalization/environment/module relationship,
+and requires byte-identical reprojection. It opens no database and performs no network access.
+
+## Status language
+
+- `ready`: the five files and their frozen-source bindings verify.
+- `Comparator-verified`: reserved for a later successful official Linux sandboxed Comparator run
+  on this exact package and toolchain.
+- `stale`: a later status layer must use when any bound challenge, solution, dependency manifest,
+  theorem source, configuration, or tool pin differs.
+
+The v1 package record can encode only `ready`, `comparator_verified: false`, and
+`authoritative: false`. A normal Lean build, offline reprojection, fake-landrun, or a green badge is
+not Comparator verification.
+
+The trust decision is recorded in
+[ADR-0014](../decisions/ADR-0014-deterministic-comparator-ready-package-boundary.md).
@@ -59,6 +59,19 @@ The full interface and output contract are documented in
 [MathCorpus and MCIP export](../implementation/CORPUS_EXPORT.md), with the trust decision in
 [ADR-0012](../decisions/ADR-0012-deterministic-offline-mathcorpus-mcip-projection.md).
 
+## Project a Comparator-ready package
+
+`mcl release export-comparator` combines an explicit reviewed challenge plan with the exact theorem
+source, formalization, and environment from a verified frozen release. It emits the five files in
+SPEC 20.3 and fixes the official tool repositories to reviewed full commits. The separate
+`verify-comparator-package` command requires trusted release and verification hashes and reproduces
+every byte without SQLite.
+
+This boundary establishes only `ready`. It cannot encode a Comparator result or authority. The
+full interface and status vocabulary are documented in
+[Comparator-ready packages](COMPARATOR_PACKAGES.md), with the trust decision in
+[ADR-0014](../decisions/ADR-0014-deterministic-comparator-ready-package-boundary.md).
+
 ## Trust boundary
 
 - A successful build means the exported directory matched canonical state at build time.

@@ -0,0 +1,22 @@
+namespace MathOS.PilotA
+
+def Prime (n : Nat) : Prop :=
+  n >= 2 ∧ ∀ d : Fin (n + 1), d.val >= 2 -> d.val < n -> n % d.val ≠ 0
+
+def Odd (n : Nat) : Prop :=
+  n % 2 = 1
+
+theorem two_is_prime_and_not_odd : Prime 2 ∧ ¬ Odd 2 := by
+  unfold Prime Odd
+  decide
+
+theorem every_prime_is_odd_refuted :
+    Not (∀ n : Nat, MathOS.PilotA.Prime n -> MathOS.PilotA.Odd n) := by
+  intro universal_claim
+  exact two_is_prime_and_not_odd.2 (universal_claim 2 two_is_prime_and_not_odd.1)
+
+theorem every_prime_other_than_two_is_odd :
+    ∀ n : Nat, MathOS.PilotA.Prime n -> n ≠ 2 -> MathOS.PilotA.Odd n := by
+  sorry
+
+end MathOS.PilotA