Mnehmos · Jul 25, 2026 · Jul 22, 2026 · Jul 25, 2026 · Jul 25, 2026
@@ -4,6 +4,7 @@
 # These vendored files are cryptographic inputs and must retain their upstream bytes.
 schemas/mathcorpus/upstream-*/* -text
 schemas/mcip/v1/upstream-*/* -text
+fixtures/comparator/authority/* -text
 
 # RL export embeds these schemas as deterministic member bytes on every platform.
 schemas/release/rl-*.schema.json text eol=lf
@@ -208,6 +208,29 @@ jobs:
           printf 'comparator_package_hash=%s\n' "$package_hash" >> "${GITHUB_OUTPUT}"
           printf 'comparator_release_hash=%s\n' "$release_hash" >> "${GITHUB_OUTPUT}"
           printf 'comparator_plan_hash=%s\n' "$plan_hash" >> "${GITHUB_OUTPUT}"
+      - name: Snapshot canonical state for the separate Comparator authority gate
+        shell: bash
+        run: |
+          set -euo pipefail
+          state_snapshot="${RUNNER_TEMP}/comparator-authority-state"
+          mkdir -- "$state_snapshot"
+          cp -a -- "${RUNNER_TEMP}/publication-candidate/.mcl" "$state_snapshot/.mcl"
+          cp -- "${RUNNER_TEMP}/publication-candidate/mcl.toml" "$state_snapshot/mcl.toml"
+          [[ -f "$state_snapshot/.mcl/state.sqlite3" \
+              && ! -L "$state_snapshot/.mcl/state.sqlite3" \
+              && -f "$state_snapshot/mcl.toml" \
+              && ! -L "$state_snapshot/mcl.toml" ]] || {
+            echo "Comparator authority state snapshot is incomplete" >&2
+            exit 71
+          }
+      - name: Transfer canonical state only to the separate authority job
+        uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
+        with:
+          name: comparator-authority-state-${{ github.sha }}
+          if-no-files-found: error
+          include-hidden-files: true
+          retention-days: 1
+          path: ${{ runner.temp }}/comparator-authority-state/
       - name: Retain smoke, candidate closures, release, exports, Comparator package, diagnostics, and Sigstore bundles
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -244,7 +267,7 @@ jobs:
     needs: boundary
     if: github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
-    timeout-minutes: 30
+    timeout-minutes: 45
     permissions:
       actions: read
       contents: read
@@ -295,6 +318,11 @@ jobs:
         with:
           name: publication-boundary-${{ github.sha }}
           path: ${{ runner.temp }}/publication-boundary
+      - name: Download canonical state for controlled Comparator ingestion
+        uses: actions/download-artifact@d3f86a106a0bac45b974a628896c90dbdf5c8093
+        with:
+          name: comparator-authority-state-${{ github.sha }}
+          path: ${{ runner.temp }}/comparator-authority-state
       - name: Install pinned attestation verifier
         shell: bash
         run: |
@@ -340,6 +368,17 @@ jobs:
             "${RUNNER_TEMP}/comparator-run/bundle/report.json" \
             "${COMPARATOR_BUNDLE_PATH}" \
             "${RUNNER_TEMP}/comparator-run-attestation-verification"
+      - name: Stage, ingest, promote, and replay Comparator authority
+        shell: bash
+        env:
+          COMPARATOR_BUNDLE_PATH: ${{ steps.attest_comparator.outputs.bundle-path }}
+        run: |
+          scripts/comparator-authority-ingest.sh \
+            "${RUNNER_TEMP}/comparator-authority-state" \
+            "${RUNNER_TEMP}/publication-boundary" \
+            "${RUNNER_TEMP}/comparator-run/bundle" \
+            "${COMPARATOR_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/comparator-authority-state/comparator-authority-output"
       - name: Retain the package, report, binaries, raw logs, verifier result, and attestation
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
@@ -356,3 +395,4 @@ jobs:
             ${{ runner.temp }}/comparator-run/work/lake-manifest-init.stderr
             ${{ runner.temp }}/comparator-run-attestation-verification/
             ${{ steps.attest_comparator.outputs.bundle-path }}
+            ${{ runner.temp }}/comparator-authority-state/comparator-authority-output/
@@ -0,0 +1,96 @@
+# ADR-0016: Comparator authority is a receipt-bound replayed evidence gate
+
+Date: 2026-07-22
+
+Status: accepted
+
+## Context
+
+ADR-0015 produces an exact protected official Comparator report and authenticates its bytes with
+GitHub OIDC provenance. The report is intentionally `authoritative: false`. Attestation proves
+where exact bytes came from; it does not establish that the named formalization, publication
+authority, fidelity witness, release, plan, package, tools, policy, and retained artifacts are
+still the current canonical closure.
+
+The existing `evidence/1` contract excludes all authoritative values. `evidence/2` has a narrower
+published meaning: an accepted Lean kernel proof or refutation bound to a publication receipt.
+Reinterpreting either version to admit Comparator authority would change the semantics of existing
+canonical hashes.
+
+## Decision
+
+MathOS adds `evidence/3` as a closed accepted authoritative `comparator_run` contract. Existing
+`evidence/1` and `evidence/2` serialized bytes, schemas, and validation remain unchanged. Version 3
+requires one `comparator_authority_binding/1`, an exact formalization and environment, a sorted
+complete artifact closure, no local run or job identity, no supersession, and no caller-authored
+staleness assertion.
+
+Authority uses three separate application operations:
+
+1. staging verifies the exact 20-file run bundle, independently reprojects the five-file package
+   from a supplied canonical plan and frozen release, rejects unsafe filesystem entries, and
+   places the exact run, release, plan, policy, and Sigstore bundle bytes in CAS under an immutable
+   non-authoritative `comparator_authority_stage/1`;
+2. ingestion re-reads only staged CAS bytes, repeats structural and semantic verification, invokes
+   only the hash- and version-pinned GitHub CLI verifier with typed repository, workflow, protected
+   ref, source and signer commit, predicate, subject, and hosted-runner constraints, parses the
+   verifier result, and creates an immutable non-authoritative
+   `comparator_attestation_verification/1` receipt; and
+3. promotion accepts only receipt hash, actor, idempotency key, and dry-run. It replays every CAS
+   member and current canonical binding, derives the evidence subject, kind, result, authority,
+   environment, verifier identity, and complete closure, and passes a non-deserializable commit to
+   a crate-private Store gate.
+
+The expensive CAS, release, package, attestation, publication-authority, and fidelity replay occurs
+before the write transaction. The short Store transaction re-reads the immutable stage and
+receipt, rechecks the current formalization head and database projections, enforces one evidence
+per receipt and idempotency, inserts the evidence, reads it back through integrity validation, and
+commits the idempotency result atomically. Immutable tables, a closed SQL insert trigger, and
+read-time projection checks provide separate defense in depth.
+
+Comparator evidence currentness is derived live. The evidence remains immutable historical fact;
+it is `current` only while the exact formalization, publication authority and fidelity witness,
+release, plan, package fingerprint, policy and tool pins, report, attestation, and every required
+CAS member replay. A changed canonical input returns a deterministic stale reason. Missing or
+corrupt bytes are integrity failures rather than ordinary staleness.
+
+Comparator authority records that an exact publication package passed the reviewed official
+Comparator boundary. It does not create Lean proof or refutation evidence, replace statement
+fidelity review, directly set `proved` or `disproved`, or complete Pilot C.
+
+## Consequences
+
+- A protected report, a successful workflow, or caller-selected hashes cannot self-promote.
+- Prior evidence versions remain portable and byte-compatible.
+- Attestation receipt creation and mathematical authority remain distinct transitions.
+- Retry, restart, direct SQL, incomplete closure, receipt reuse, current-head races, and later
+  projection tampering fail closed under separate controls.
+- Historical Comparator acceptance remains auditable after it becomes stale for current use.
+- Promotion is intentionally more expensive than a projection insert because it replays the exact
+  portable evidence chain.
+
+## Rejected alternatives
+
+### Extend `evidence/2`
+
+Rejected because version 2 is already the closed publication-bound Lean proof/refutation contract.
+
+### Trust the report's `comparator_verified` field
+
+Rejected because the report generator and workflow are evidence producers, not the canonical
+authority gate.
+
+### Treat attestation verification as promotion
+
+Rejected because authentic bytes may still name stale, substituted, or incomplete canonical
+inputs.
+
+### Persist a mutable stale flag
+
+Rejected because currentness depends on independently versioned live chains. It is derived by
+replay and never rewritten into historical evidence.
+
+### Let callers construct `evidence/3`
+
+Rejected because caller selection of the subject, environment, result, binding, or artifact set
+would recreate a generic authority mutation API.
@@ -1,6 +1,6 @@
 # MathOS 1.0.0 Release Checklist
 
-Last updated: 2026-07-21
+Last updated: 2026-07-22
 
 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.
 
@@ -112,7 +112,11 @@ Downloaded artifact `8517692129`, `publication-boundary-4b0a740b666e5e020b25e078
 
 Phase 6d Comparator-package issue [#60](https://github.com/Mnehmos/MathOS/issues/60) completed through PR [#61](https://github.com/Mnehmos/MathOS/pull/61). 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. Reviewed head `36ae9586dc7985785501474c53e1ee3d6067b5f5` merged as `2fe5d00992599a2c22a974c01ec0cdc4fbea286d`; exact-head CI `29893380402`, merged-tree CI `29893579467`, and protected publication run `29893579466` passed.
 
-Artifact `8519152437`, `publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbea286d`, is 478,926 archive bytes with GitHub SHA-256 `642edf93c509407efe953a4dda588fe3190bf7bc66204d03fe1387b9a7e31384`; it expands to 373 files and 895,683 bytes with no links or reparse points. Independent audit reproduced the exact five-file, 6,095-byte package from source release `f268d9da8fa4e19a05ac32d1c85b14e9e427db326dc9a69553b1bb11d3366eff` and canonical plan `a9048a8ac02907993cd1114e3c06510524933c72b891c786d15d5beeb82c7088`. Every package/source hash and binding matched input fingerprint `aee3e4e65754205932caa8cca0937d017965bb7936d7d1cec86117e1d7225898` and verification `beef8cd5d48d9cee07352f34366db5f34c77bc73b9c685b83ded490618960758`; canonical JSON, parsed YAML, exact solution lineage, fixed tool pins, nonexistent-root reprojection, and both Lean files passed. It is only `ready`; verification and authority remain structurally false. Real protected Linux Comparator execution remains open and no full Comparator verification criterion is checked.
+Artifact `8519152437`, `publication-boundary-2fe5d00992599a2c22a974c01ec0cdc4fbea286d`, is 478,926 archive bytes with GitHub SHA-256 `642edf93c509407efe953a4dda588fe3190bf7bc66204d03fe1387b9a7e31384`; it expands to 373 files and 895,683 bytes with no links or reparse points. Independent audit reproduced the exact five-file, 6,095-byte package from source release `f268d9da8fa4e19a05ac32d1c85b14e9e427db326dc9a69553b1bb11d3366eff` and canonical plan `a9048a8ac02907993cd1114e3c06510524933c72b891c786d15d5beeb82c7088`. Every package/source hash and binding matched input fingerprint `aee3e4e65754205932caa8cca0937d017965bb7936d7d1cec86117e1d7225898` and verification `beef8cd5d48d9cee07352f34366db5f34c77bc73b9c685b83ded490618960758`; canonical JSON, parsed YAML, exact solution lineage, fixed tool pins, nonexistent-root reprojection, and both Lean files passed. At that checkpoint it was only `ready`; protected execution and authority remained separate later transitions. Phase 6e execution evidence follows.
+
+Phase 6e Comparator-execution issue [#63](https://github.com/Mnehmos/MathOS/issues/63) completed through PR [#64](https://github.com/Mnehmos/MathOS/pull/64), merge `3a75ddc8bc5de685dc6425d6158791553be0ca40`. Exact-head CI `29898468563`, merged-tree CI `29898749801`, and protected publication run `29898749807` passed. Downloaded artifact `8521103391` independently verified the exact 20-file official run bundle without SQLite: report `42b29ecd69b222c26e1de47bed83f6e3e8df5910f35f1c2543a2d9ed72eb3198`, package verification `7a3adfa8e30085cbda8ca240ab8288909a088d7ae0f9880ba0cc5b410645cc52`, attestation bundle `a447696ceeb6e537c0bc6e5ebf81ab95d2e91006df57aa2bb632edc60d4cf0a5`, and artifact digest `sha256:f322f92281ea6cc70f70cdc657d32a2029f559328be50c434ef857e4714403ba`. The accepted report proves the scoped official execution boundary only and remains `authoritative: false`.
+
+Phase 6f issue [#65](https://github.com/Mnehmos/MathOS/issues/65) has an implementation candidate for the separate authority transition: byte-compatible evidence v1/v2 plus closed `evidence/3`, exact CAS staging and reprojection, pinned constrained attestation receipt, receipt-only derived promotion, immutable Store and SQL defenses, live current/stale replay, and one CLI/MCP application path. Comparator evidence is deliberately excluded from Lean proof/refutation claim-status inputs. The scoped checklist evidence remains provisional until exact-head CI, a protected same-run promotion, and an independent database-free retained-artifact audit pass.
 
 ## Migration