Mnehmos · Jul 21, 2026 · Jul 21, 2026
@@ -29,12 +29,12 @@ Remote fidelity evidence: GitHub Actions run `29706138708` passed fresh Linux, W
 
 Phase 3 derived-status evidence: issue #38 preserves fidelity v1 canonical identity, adds closed polarity-aware fidelity v2, and derives one exact claim's live status through the same CLI/MCP application service. Callers provide only exact claim identity. The Store automatically captures every current formalization plus source/claim/formalization/fidelity/authority heads in one read snapshot; the application rehashes canonical records and all fidelity CAS, fully replays every receipt-bound protected authority chain, then rejects mixed-time reads on basis change. Proof/refutation fixtures, v1-negation refusal, v2 relation mismatch, superseded claim and formalization heads, moved-source invalidation, restart determinism, and missing-CAS failure pass. The protected publication workflow retains `open` after authority and `proved` only after role-separated verified v2 fidelity. Exact merged-tree CI and the protected artifact have been independently audited, satisfying the truth-derivation item; the broader counterexample, repair, pedagogy, replay, and release lifecycle remains incomplete.
 
-Pilot A refutation candidate evidence: issue #41 commits an exact no-import Lean module for “Every prime number is odd,” including a named checked witness that `2` is prime and not odd and a negation theorem that uses it. The protected producer creates the exact source, normalized universal natural-number claim, negation-polarity formalization, local evidence, and refutation request through `mcl`; its staging, ingestion, authority, v2 logical-negation fidelity, and derived-status path remains unchanged. A Windows CLI playtest completed elaboration and axiom-free audit, prepared the refutation request, and rejected a proof request for the same formalization. The broad lifecycle and Pilot A boxes remain open until protected merged-tree refutation evidence is independently audited and counterexample packaging, repair, repaired proof, pedagogy, and export are implemented.
+Pilot A refutation evidence: issue #41 and PR #42 commit an exact no-import Lean module for “Every prime number is odd,” including a named checked witness that `2` is prime and not odd and a negation theorem that uses it. The protected producer creates the exact source, normalized universal natural-number claim, negation-polarity formalization, local evidence, and refutation request through `mcl`; its staging, ingestion, authority, v2 logical-negation fidelity, and derived-status path remains unchanged. A Windows CLI playtest completed elaboration and axiom-free audit, prepared the refutation request, and rejected a proof request for the same formalization. Exact-head CI, merged-tree CI, and the protected publication run passed; the retained artifact was independently audited through authoritative refutation, distinct-reviewer logical-negation fidelity, and the derived `disproved` read. This satisfies the exact proof-and-refutation evidence item only. The broad lifecycle and Pilot A boxes remain open until counterexample packaging, immutable repair, repaired proof, pedagogy, and export are implemented.
 
 ## Verification
 
 - [x] Lean verification uses pinned environments.
-- [ ] Authoritative proof and refutation evidence is recorded against exact formalization versions.
+- [x] Authoritative proof and refutation evidence is recorded against exact formalization versions.
 - [x] Hole, unsafe, and axiom policies are enforced.
 - [ ] Replay works and reports its exact trust boundary.
 - [x] Publication CI produces retained evidence.
@@ -55,7 +55,7 @@ Phase 3 local audit evidence: the committed audit policy and closed request/repo
 
 Phase 3 publication contract evidence: the closed publication policy, request, retained closure, candidate report, quarantine stage, canonical CAS attestation-verification record (`publication_attestation_verification/1`), and separate immutable SQLite ingestion receipt (`PublicationIngestionReceiptSnapshot` in `publication_ingestion_receipts`) bind exact proof or refutation intent, diagnostic and audit evidence, formalization, environment, module, declaration, Git commit and tree, protected workflow identity, runner class, required isolation controls, retained artifacts, and SHA-pinned attestation actions and verifier. The application derives canonical private request artifacts from the current formalization head and one exact accepted elaboration/audit chain without accepting request JSON or authority fields. Typed formalization polarity prevents one exact version/evidence closure from being requested as both proof and refutation; legacy records without polarity cannot publish until versioned and reverified. The workflow-facing validator and staging path require 25 exact fixed-path closure roles, recompute every member hash, and revalidate the source, claim, formalization, evidence, job, report, policy, environment, module, parser-derived protected dependency output, and local/protected axiom relationships. Hash-only CLI and MCP ingestion resolve that immutable stage, run an isolated copy of the Linux-amd64 SHA-pinned GitHub CLI with fixed arguments, parse one closed attestation result, retain the raw output and canonical CAS attestation-verification record, then register the separate immutable SQLite ingestion receipt plus the logical stage/actor idempotency result in one final transaction that rechecks currentness. Missing or altered CAS, stale state, key rebinding, parser ambiguity, and unpinned or misbehaving verifiers fail closed. The protected producer fails unless GitHub reports an actively protected source ref, then builds a real no-import candidate under clean-checkout, Bubblewrap network/process isolation, timeout, memory, and output-size controls; pull-request CI runs it without attestation, while protected `main` attests the exact candidate report. Every request, report, stage, validation result, attestation-verification record, and ingestion receipt remains structurally non-authoritative. The attestation-verification record and its ingestion receipt prove provenance only and may not be treated as a passed report or proof. Merged-tree controlled-ingestion evidence is complete and recorded below.
 
-Phase 3 authority-gate evidence: closed `evidence/2` and nested `publication_authority_binding/1` contracts preserve `evidence/1` identities while allowing only accepted authoritative Lean kernel proof/refutation evidence with a complete receipt-bound CAS closure. Hash-only CLI and MCP promotion accept only an ingestion receipt hash plus attribution. The application revalidates the report, closure, all 25 members, bundle, raw output, canonical receipt, current Store snapshots, request derivation, and attestation parser; explicitly requires a `passed` report; and derives evidence kind from typed polarity. Controlled ingestion immutably binds the receipt's exact subject to the registered private generated publication-request artifact. The Store accepts only a non-deserializable derived commit and uses one immediate transaction to recheck that receipt/request/subject relationship, stage projections, current head, environment, polarity, uniqueness, and idempotency. Migration 0011 rejects every kernel/authoritative/v2 row outside the fixed shape. Statement fidelity is intentionally not an authority input; a later truth read must combine current fidelity with current proof authority. One exact protected proof record is now independently audited. The proof/refutation checkbox remains conservative until a protected refutation artifact is also recorded; the separate refutation type and Store path are already adversarially tested. Full SPEC replay remains a separate open capability.
+Phase 3 authority-gate evidence: closed `evidence/2` and nested `publication_authority_binding/1` contracts preserve `evidence/1` identities while allowing only accepted authoritative Lean kernel proof/refutation evidence with a complete receipt-bound CAS closure. Hash-only CLI and MCP promotion accept only an ingestion receipt hash plus attribution. The application revalidates the report, closure, all 25 members, bundle, raw output, canonical receipt, current Store snapshots, request derivation, and attestation parser; explicitly requires a `passed` report; and derives evidence kind from typed polarity. Controlled ingestion immutably binds the receipt's exact subject to the registered private generated publication-request artifact. The Store accepts only a non-deserializable derived commit and uses one immediate transaction to recheck that receipt/request/subject relationship, stage projections, current head, environment, polarity, uniqueness, and idempotency. Migration 0011 rejects every kernel/authoritative/v2 row outside the fixed shape. Statement fidelity is intentionally not an authority input; a later truth read must combine current fidelity with current proof authority. One exact protected proof and one exact protected refutation are now independently audited against distinct exact formalization versions, satisfying only the proof/refutation evidence item above. Counterexample repair, the full claim lifecycle, and full SPEC replay remain open capabilities.
 
 Remote controlled-ingestion evidence: PR #34 merged as `95bd8a1d2068612b5eca644c3d77754b5e4f49fd`, tree `4027d03fe05bd997108c86250adcf2d920adda48`; main CI run `29721420110` passed all five jobs. Protected publication run `29721420136`, job `88285050682`, passed exact candidate construction, attestation, independent challenge, staging, controlled ingestion, and retention. Artifact `8452528096` has GitHub archive digest `66cd47753a77f90bf216b874d4d7c99f7ba561a4586e29c524e094c82eb3206c`. Downloaded inspection recomputed the report (`5f02696eac1308f48eae9f085f003e750f009dbe496d055543792b088e3b2aa6`), 25-role closure (`6440836d612d91dfe43af952d6ac83ca1445bf75c86b8b52a8c79f6121427b38`), candidate bundle (`c02cde0384cd015bbb085d2f98e69c245888dd7cfbc10973b0c9a9e722ad326c`), stage (`e4b307416358ef657c57d81d07c6b21df0381befbf5600982442bc435d98baa5`), raw verifier output (`bdfe54e9e889c52c7dc32941dc8fb16d50b1e2b8071a5b69be04eb1040d45932`), and canonical CAS attestation-verification/SQLite receipt key (`659b789a41a14ac59ca9253c2c71d73c4717acc58dcc2187809e92c710814402`) hashes. All 71 retained files, eight stderr files, immutable repository/owner identities, one subject, one source dependency, Rekor timestamp `2026-07-20T06:22:33Z`, and 18 false authority fields passed audit. This is exact provenance evidence only.

@@ -67,6 +67,10 @@ Remote derived-status evidence: PR #39 merged final reviewed head `849dce08a84f7
 
 The independent audit matched every archive member and all 25 closure roles; parsed 54 JSON files plus 25 JSONL closure entries; and recomputed report `6fdd7982316e28be2dd7a69b2ec743a37cae5479807e77ee00db749e9499b09b`, closure `4e2acef7c87d19421e0305eb1dcfbd7cf5bc6e701528bd815799cc008fc8a7bb`, stage `6036e9c90cf8edc550e898912bdd2a8672e3b76cd4ba6ba31318e5f9378dc2e5`, receipt `61b804b1888f71346e15e6e96452af58a34703507cdbf9d637834b0272ae1cf1`, bundle `27fbff08373c79d348b85495ba7e6c821386060bfb4c8f247cce3ab83528e217`, and raw-verification `fca79f52d98c047dde52f49c6d0e417506c30b27bccfe97ffdb316204fa0391e` identities. The exact claim first returns `open/no_current_verified_fidelity` with authoritative proof present, then returns `proved` with one witness only after distinct reviewer `protected-fidelity-reviewer` records v2 `claim` request `b12e35aca5c921e5af0cc8b1f6b7aebff3b20f2cc0467cb79ee89961ca554785`, report `c0a74cda75ab6e919c3b216a4d0b247bd3bd7133c088293827ec034490ae0708`, and reviewed evidence `afb6304b0af81b8dc18a51d41636519b5276e30ce73fdff2eb57c3af5eb5bdb3`. The attestation binds the exact protected workflow, commit, run, hosted runner, repository IDs, and Rekor timestamp `2026-07-21T18:19:58Z`. No Boolean authority assertion exists; the sole authoritative semantic is the accepted receipt-bound `evidence/2.authority_class`.
 
+Remote Pilot A refutation evidence: PR #42 merged final reviewed head `1a5755fa815ca187c594e1d4db0c488d0a5e327c` as `18abdd23025cc245f0b5722a8676e5b3f1bb2237`, tree `8945fd4746c1f9d9d536dd14d17854da3c9d0bdd`. Exact-head PR run `29860329570` and main run `29860589159` passed all five required jobs. Protected publication run `29860588969`, job `88735987761`, retained the full refutation-authority, role-separated fidelity, and before/after status path. Artifact `8507149183` contains 78 files, is 89,176 archive bytes, and has GitHub and independently downloaded SHA-256 `7172aa87bccedf6a694299d076e6279061cd541cf5d4b8625d01bb7e0ba3b87f`.
+
+The independent audit matched all archive members and 25 closure roles; parsed 54 JSON files plus 25 JSONL entries; verified exact committed module hash `1e011925f7444a635c263725bf5f7dfc6fabdcd17c6f7e97135b22a534cc5af3` and the empty axiom set; and recomputed request `513ed6ddb73294d03e8225298ef1f94b123434b52fa65da3540ead4a8ca88e7d`, report `0ab1aa3c7e46814b06d235987caa0b0fae7cf146ff717697ceafcb8ff625a106`, closure `85a72971c8715c7998492143a0e63db18fae06da7283d1d8be313c66d036f340`, bundle `2f82f4c28c76736ce65597608f33b9ddf719a6bc4dc213e80b92c8008b5aca9f`, stage `1ec7bbd2054173bba8cb310e66fbfc7dcff47171416ffd80ce0b02034197461d`, raw verification `089af2f16be942bbb58995df745165ce4bba2f4a6273fd7955446974484045df`, and receipt `46d88e197a040be6ce851fb28f980aee1f4dfda7714e304e5dd6e807405aaa52`. Accepted authoritative `lean_kernel_refutation` evidence `52484265b0cae459cca257b95cbec4f00033987929ff7394b3db3ffa547d9225` names exact negation formalization version `1f9621d15a83cbf3c201cd6d3cc739f4624cee59fdc103cf603b94f86ebac0b9`; distinct-reviewer `logical_negation` evidence `8d809395a76a5c23b126053d6b70e40a398d346a876b821ee25d9cbcf2119bfc` changes the exact claim read 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, commit, run, hosted runner, repository IDs, and Rekor timestamp `2026-07-21T19:14:47Z`.
+
 Remote local-audit evidence: GitHub Actions run `29704542965` passed the exact real Lean audit lifecycle and fresh Linux and Windows suites on tree `30d55d6e2ce7b0de2d921cff3e1368124fd9f66f`. That checkpoint validates local diagnostics only; the later protected authority evidence above is the basis for the checked pin and policy items, not for the still-open SPEC replay item.
 
 Remote request-preparation evidence: PR #30 merged as `da33431a1061bb3f05db7a7d2473f1fb5b8059f2`, tree `620f2a3060290ffe37fb3051ff604fa4433679af`. Main CI run `29711916515` passed every required platform/toolchain job; publication run `29711916501` retained and independently verified the exact non-authoritative smoke artifact. That request-preparation capability is now incorporated into the merged candidate and controlled-ingestion evidence above.