Mnehmos · Jul 21, 2026 · Jul 21, 2026 · Jul 21, 2026 · Jul 21, 2026
@@ -78,6 +78,18 @@ jobs:
           set -euo pipefail
           lean --version | tee "${RUNNER_TEMP}/lean-version.txt"
           grep --fixed-strings "Lean (version 4.32.0," "${RUNNER_TEMP}/lean-version.txt"
+      - name: Prove the repaired Pilot A theorem has no axioms
+        shell: bash
+        run: |
+          set -euo pipefail
+          driver="${RUNNER_TEMP}/PilotARepairedProofAudit.lean"
+          output="${RUNNER_TEMP}/PilotARepairedProofAudit.txt"
+          cp fixtures/publication/PilotARefutation.lean "${driver}"
+          printf '\n#print axioms MathOS.PilotA.every_prime_other_than_two_is_odd\n' >>"${driver}"
+          lean -DwarningAsError=true "${driver}" 2>&1 | tee "${output}"
+          grep --fixed-strings --line-regexp \
+            "'MathOS.PilotA.every_prime_other_than_two_is_odd' does not depend on any axioms" \
+            "${output}"
       - name: Install publication isolation control
         shell: bash
         run: |
@@ -112,7 +124,20 @@ jobs:
           cargo build --locked --bin mcl
           export PUBLICATION_SOURCE_TREE_SHA
           PUBLICATION_SOURCE_TREE_SHA="$(git rev-parse 'HEAD^{tree}')"
-          bash scripts/publication-candidate.sh "${RUNNER_TEMP}/publication-candidate-simulated-main"
+          candidate="${RUNNER_TEMP}/publication-candidate-simulated-main"
+          bash scripts/publication-candidate.sh "${candidate}"
+          if bash scripts/publication-candidate.sh \
+            "${candidate}/repaired-proof-without-repair" \
+            repaired-proof \
+            "${candidate}" \
+            >"${RUNNER_TEMP}/unexpected-repaired-proof.json" \
+            2>"${RUNNER_TEMP}/expected-missing-repair.txt"; then
+            echo "repaired proof candidate was created without the atomic repair" >&2
+            exit 1
+          fi
+          grep --fixed-strings \
+            "repaired proof requires the retained atomic repair in canonical state" \
+            "${RUNNER_TEMP}/expected-missing-repair.txt"
       - name: Exercise staged-CAS ingestion barrier without authority
         shell: bash
         run: |
@@ -201,6 +226,7 @@ jobs:
             ${{ runner.temp }}/publication-candidate-simulated-main/closure/
             ${{ runner.temp }}/publication-candidate-simulated-main/publication-retained-closure.json
             ${{ runner.temp }}/publication-candidate-simulated-main/publication-report.json
+            ${{ runner.temp }}/publication-candidate-simulated-main/repaired-proof-without-repair/attempt/
 
   legacy-python-regression:
     name: Legacy Python regression evidence

@@ -17,7 +17,7 @@ jobs:
     name: Attested publication candidate boundary
     if: github.ref == 'refs/heads/main'
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    timeout-minutes: 20
     permissions:
       contents: read
       id-token: write
@@ -136,8 +136,53 @@ jobs:
           scripts/publication-ingest.sh \
             "${RUNNER_TEMP}/publication-candidate" \
             "${CANDIDATE_BUNDLE_PATH}" \
-            "${RUNNER_TEMP}/publication-candidate-ingestion"
-      - name: Retain smoke, candidate closure, diagnostics, and Sigstore bundles
+            "${RUNNER_TEMP}/publication-candidate/refutation-ingestion"
+      - name: Build and validate the repaired claim proof in canonical state
+        shell: bash
+        env:
+          PUBLICATION_CONTEXT_MODE: protected-main
+          PUBLICATION_REPOSITORY: ${{ github.repository }}
+          PUBLICATION_WORKFLOW_PATH: .github/workflows/publication.yml
+          PUBLICATION_WORKFLOW_REF: ${{ github.workflow_ref }}
+          PUBLICATION_SOURCE_REF: ${{ github.ref }}
+          PUBLICATION_SOURCE_COMMIT_SHA: ${{ github.sha }}
+          PUBLICATION_WORKFLOW_RUN_ID: ${{ github.run_id }}
+          PUBLICATION_WORKFLOW_RUN_ATTEMPT: ${{ github.run_attempt }}
+          PUBLICATION_RUNNER_ENVIRONMENT: github_hosted
+        run: |
+          set -euo pipefail
+          export PUBLICATION_SOURCE_TREE_SHA
+          PUBLICATION_SOURCE_TREE_SHA="$(git rev-parse 'HEAD^{tree}')"
+          bash scripts/publication-candidate.sh \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-candidate" \
+            repaired-proof \
+            "${RUNNER_TEMP}/publication-candidate"
+      - name: Attest exact repaired claim proof report
+        id: attest_repaired_proof
+        uses: actions/attest@59d89421af93a897026c735860bf21b6eb4f7b26
+        with:
+          subject-path: ${{ runner.temp }}/publication-candidate/repaired-proof-candidate/publication-report.json
+      - name: Verify exact repaired proof attestation and retain the challenge result
+        shell: bash
+        env:
+          PUBLICATION_GH_BIN: ${{ runner.temp }}/gh_2.96.0_linux_amd64/bin/gh
+          REPAIRED_PROOF_BUNDLE_PATH: ${{ steps.attest_repaired_proof.outputs.bundle-path }}
+        run: |
+          scripts/publication-attestation-verify.sh \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-candidate/publication-report.json" \
+            "${REPAIRED_PROOF_BUNDLE_PATH}" \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-attestation-verification"
+      - name: Ingest and promote the repaired proof without inherited evidence
+        shell: bash
+        env:
+          REPAIRED_PROOF_BUNDLE_PATH: ${{ steps.attest_repaired_proof.outputs.bundle-path }}
+        run: |
+          scripts/publication-ingest.sh \
+            "${RUNNER_TEMP}/publication-candidate/repaired-proof-candidate" \
+            "${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
         if: always()
         uses: actions/upload-artifact@ea165f8d65b6e75b540449e92b4886f43607fa02
         with:
@@ -153,5 +198,12 @@ jobs:
             ${{ runner.temp }}/publication-candidate/publication-retained-closure.json
             ${{ runner.temp }}/publication-candidate/publication-report.json
             ${{ runner.temp }}/publication-candidate-attestation-verification/
-            ${{ runner.temp }}/publication-candidate-ingestion/
+            ${{ runner.temp }}/publication-candidate/refutation-ingestion/
             ${{ steps.attest_candidate.outputs.bundle-path }}
+            ${{ runner.temp }}/publication-candidate/repaired-proof-candidate/attempt/
+            ${{ runner.temp }}/publication-candidate/repaired-proof-candidate/closure/
+            ${{ runner.temp }}/publication-candidate/repaired-proof-candidate/publication-retained-closure.json
+            ${{ runner.temp }}/publication-candidate/repaired-proof-candidate/publication-report.json
+            ${{ runner.temp }}/publication-candidate/repaired-proof-attestation-verification/
+            ${{ runner.temp }}/publication-candidate/repaired-proof-ingestion/
+            ${{ steps.attest_repaired_proof.outputs.bundle-path }}
@@ -14,7 +14,9 @@ Phase 3 formalization now has independently audited protected proof-authority an
 
 The merged issue #38 slice preserves fidelity v1 identities, adds polarity-aware fidelity request/report v2, and introduces one closed `claim_research_status/1` response shared by CLI and MCP. The application rehashes exact source, claim, and every current formalization; strictly replays the complete fidelity history and every receipt-bound authority chain; captures and rechecks source, claim, formalization, fidelity, and authority identities; and returns exact witnesses or explicit nonqualification reasons. Full proof and refutation fixtures establish that authority without fidelity remains `open`, v1 cannot support source disproof, v2 logical-negation fidelity plus protected refutation derives `disproved`, a moved source head invalidates a formerly terminal witness as `open/source_version_not_current`, and changed heads or missing CAS fail closed. The protected workflow retains an `open` CLI result after authority and a terminal CLI result only after a separate reviewer role submits verified v2 fidelity. Exact merged-tree evidence is recorded below.
 
-The issue [#44](https://github.com/Mnehmos/MathOS/issues/44) slice implements the next Pilot A boundary without claiming proof of the repair. Closed counterexample request/package contracts feed one application-only operation that replays the current `disproved` basis and exact counterexample-search chain, derives the checker and evidence locators, stages canonical package bytes, and atomically registers the artifact, a new claim object, its controlled `research.repairs` edge, and one idempotency result. The original claim remains untouched and `disproved`; the repaired claim begins independently as `not_started`. CLI and MCP share the operation, generic repair-edge creation is denied, transaction-fault and concurrent-head tests prove rollback/conflict behavior, and the protected producer now retains witness `2`, exact package bytes, the new claim, edge, retry, retrieval replay, and both post-repair status reads. Merged-tree CI, protected publication, and independent downloaded-artifact audit remain required before this checkpoint is recorded as complete.
+The issue [#44](https://github.com/Mnehmos/MathOS/issues/44) slice completed the next Pilot A boundary without claiming proof of the repair. Closed counterexample request/package contracts feed one application-only operation that replays the current `disproved` basis and exact counterexample-search chain, derives the checker and evidence locators, stages canonical package bytes, and atomically registers the artifact, a new claim object, its controlled `research.repairs` edge, and one idempotency result. The original claim remains untouched and `disproved`; the repaired claim begins independently as `not_started`. CLI and MCP share the operation, generic repair-edge creation is denied, transaction-fault and concurrent-head tests prove rollback/conflict behavior, and the protected producer retains witness `2`, exact package bytes, the new claim, edge, retry, retrieval replay, and both post-repair status reads. PR #45, merged-tree CI, protected publication, and the independently downloaded 91-file artifact all passed exact-identity audit; evidence is recorded below.
+
+Issue [#46](https://github.com/Mnehmos/MathOS/issues/46) is the current narrow slice. It must prove the repaired claim through a new claim-polarity formalization and a second retained, attested candidate in the same canonical state, create distinct protected proof authority and role-separated `claim` fidelity, derive `proved`, and demonstrate that the original claim, refutation witness, package, repair edge, and `disproved` status remain byte-identical. This does not include pedagogy, export, all of Pilot A, or MathOS 1.0 completion.
 
 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.
 
@@ -220,12 +222,14 @@ These items establish only part of the product foundation and trace model. One e
 - PR #42 merged final reviewed head `1a5755fa815ca187c594e1d4db0c488d0a5e327c` as `18abdd23025cc245f0b5722a8676e5b3f1bb2237`, tree `8945fd4746c1f9d9d536dd14d17854da3c9d0bdd`. Exact-head PR run `29860329570` and post-merge main run `29860589159` passed all five required jobs. Protected publication run `29860588969`, job `88735987761`, passed the protected-ref gate, real contained Lean refutation, attestation and independent challenge, staging, controlled ingestion, authority promotion, role-separated logical-negation fidelity review, both status reads, and retention.
 - Artifact `8507149183`, `publication-boundary-18abdd23025cc245f0b5722a8676e5b3f1bb2237`, contains 78 files and is 89,176 archive bytes. GitHub's digest and an independently downloaded ZIP both equal `7172aa87bccedf6a694299d076e6279061cd541cf5d4b8625d01bb7e0ba3b87f`. Independent audit matched every archive member and all 25 closure roles; parsed all 54 JSON files and 25 JSONL closure entries; verified the exact committed module bytes and empty axiom set; and recomputed request `513ed6ddb73294d03e8225298ef1f94b123434b52fa65da3540ead4a8ca88e7d`, report `0ab1aa3c7e46814b06d235987caa0b0fae7cf146ff717697ceafcb8ff625a106`, closure `85a72971c8715c7998492143a0e63db18fae06da7283d1d8be313c66d036f340`, bundle `2f82f4c28c76736ce65597608f33b9ddf719a6bc4dc213e80b92c8008b5aca9f`, stage `1ec7bbd2054173bba8cb310e66fbfc7dcff47171416ffd80ce0b02034197461d`, raw verification `089af2f16be942bbb58995df745165ce4bba2f4a6273fd7955446974484045df`, and receipt `46d88e197a040be6ce851fb28f980aee1f4dfda7714e304e5dd6e807405aaa52`.
 - The protected lineage names claim `019f861a-1706-7981-9f4f-0ed1231ef72c` at version `739c66af9a18a882b5c988bb3f4eb658c87c24a4a0e2f559572b39448a67d1a7` and negation formalization `019f861a-171a-7b22-abe8-45cd917bc797` at version `1f9621d15a83cbf3c201cd6d3cc739f4624cee59fdc103cf603b94f86ebac0b9`. Final evidence `019f861a-4b93-7a11-98e7-9e39aaa18192` / `52484265b0cae459cca257b95cbec4f00033987929ff7394b3db3ffa547d9225` is accepted authoritative `lean_kernel_refutation`; separate reviewer evidence `019f861a-4c13-7932-9257-83c145aa28eb` / `8d809395a76a5c23b126053d6b70e40a398d346a876b821ee25d9cbcf2119bfc` records `logical_negation`; and the exact claim changes from `open/no_current_verified_fidelity` to `disproved` with one refutation witness. No Boolean authority assertion exists, exactly one class is authoritative, all eight stderr files are empty, and the attestation binds the exact protected workflow, repository IDs, commit, run, hosted runner, and Rekor timestamp `2026-07-21T19:14:47Z`.
+- PR #45 merged reviewed head `a255608aae1abf31bea27d6a11d26e08d18f0b22` as `1e9066f01ed75ba30156718710d2451db4f7a4a8`, tree `903811d22a4bcc1bff7b50ec06186a44d6a26fb6`. Exact-head CI run `29866239855`, merged-tree CI run `29866704074`, and protected publication run `29866704122` all passed. Artifact `8509521719`, `publication-boundary-1e9066f01ed75ba30156718710d2451db4f7a4a8`, contains 91 files and 67 JSON documents; every one of its eight stderr files is empty.
+- Independent replay of that artifact verified the exact commit, tree, run, Sigstore certificate, source/claim/formalization/module hashes, authority, fidelity, receipt, complete counterexample-search event chain, result binding, canonical request and package bytes, artifact metadata, atomic repair, dry-run, persistence, retry, retrieval, and both statuses. Package `14bff23f2e7afe79d2fec05fa5d4d89a0340151398529e322e7112fd7dc83652` binds `Nat` witness `2` and result event `7e6627025dc9ed2ccd91eeb0ae08205babedea1d6c6ee17832aec28e5c0a008c`. Original claim `019f8669-1b1e-7c32-8280-2bcaf4aa01f4` / `f40843ae3c953ffd076d669ea878b7c0efad4e5fa92351114763b7e56460b237` remains byte-identically `disproved`; repaired claim `019f8669-622f-73c3-8ca7-cb5f15da829d` / `f7d4cdccc4e5be9d78991a5095d80b1eb7bf5a4e5ccffe8c1454d90377d2bb88` has no predecessor and starts `not_started`; repair edge `019f8669-6230-7c01-9011-26ad0e840f3d` preserves that immutable lineage.
 
 ## Next highest-priority criteria
 
-1. Add the Pilot A counterexample package and an atomic immutable repaired-claim path linked to the disproved claim and its exact witness.
-2. Prove and publish authority plus fidelity for the repaired Pilot A claim without mutating the disproved claim's history.
-3. Continue Pilot A pedagogy/export and the remaining section 30 criteria without treating this partial path as MathOS 1.0.
+1. Complete issue #46: prove and publish authority plus fidelity for the repaired Pilot A claim without mutating or inheriting the disproved claim's history.
+2. Continue Pilot A pedagogy and export after the repaired proof has merged and passed independent protected-artifact audit.
+3. Continue the remaining section 30 criteria without treating this partial path as MathOS 1.0.
 
 ## Exact last validation commands