Mnehmos · Jul 21, 2026 · Jul 21, 2026
@@ -20,14 +20,14 @@ Phase 2 evidence: `mcl init` and storage health work locally and in Windows and
 - [ ] Multiple formalizations per claim work end to end.
 - [ ] Fidelity review works end to end.
 - [ ] Counterexample, repair, proof, disproof, and open outcomes work end to end.
-- [ ] Truth status is derived and cannot be directly mutated.
+- [x] Truth status is derived and cannot be directly mutated.
 - [ ] Verified intermediate results can be promoted and searched.
 
 Phase 3 fidelity evidence: closed request and report types distinguish all specified review levels, attestation, benchmark alignment, verified review, rejection, ambiguity disposition, definition mappings, and exact source, claim, formalization, run, artifact, and supersession references. Reviews persist through one shared CLI and MCP application path. Controlled private reports bind human-review provenance, derived status follows one compare-and-swap evidence head, and superseded reviews remain visible. Self-verification, stale heads, missing artifacts, substituted lineage, erased ambiguity, report corruption, restart, and retry paths are tested. Fidelity is only one part of the full claim lifecycle, so the complete core lifecycle criteria remain unchecked.
 
 Remote fidelity evidence: GitHub Actions run `29706138708` passed fresh Linux, Windows, storage, Python, and real pinned Lean jobs on exact tree `80b1d2e92e81192a2863bb445a7bef872fc21b72`. Issue #20 is closed. At that checkpoint proof authority and derived mathematical status were absent; the authority evidence below now supplies only the former, so the complete lifecycle criteria remain unchecked.
 
-Phase 3 derived-status candidate: 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 are covered locally. The protected publication workflow is prepared to retain `open` after authority and `proved` or `disproved` only after role-separated verified v2 fidelity. The checklist remains open until exact merged-tree CI and protected artifacts are audited, and because the broader counterexample/repair/open lifecycle is still incomplete.
+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.
 
 ## Verification
 
@@ -61,6 +61,10 @@ Remote authority evidence: PR #36 merged as `0ef8a132dfb99e63238325ac035de948e89
 
 The independent audit recomputed the request (`3cfe3ebfa30e4446b659081cc8874ccbca684fd51d3b2c53a98b1534423a501c`), policy (`5e9f69968913a7f1f716baa1a1e548f27d5d6958582e75278b37f3fac245f167`), report (`31934fcc89b045f04f57d4a0807c0f599d188887be56507f296a9fe4d8c9e643`), 25-role closure (`20059d3ab54b2e075a7476250cf4de73f9a6c8196dd0005a7a96281d789c87df`), bundle (`99850335bf53d095653fbf59b777cbcc9c33d6fe0a769d71f3c5b8701aa9b42f`), stage (`527e4db5e0852268e1eda4d9dc5aa0e32432c6ac76e2b06f130e16aac7dbc9c6`), raw verification (`6adc6e41385249651adf372ece8334c650013b549093587891b36cafa7087453`), and receipt (`56166a02475a1d47be9013a024693bc3228801ad98d62c65fca06e6aebd90e40`) identities. Final evidence `019f7e90-7adb-7f03-8e37-e591b13eac4d` has canonical hash `dbaecfb7163476b98aead72d742891c7d8502494e81bf37e81aa5b214a9ef8cc`, kind/result/class `lean_kernel_proof` / `accepted` / `authoritative`, and an exact nine-field binding to that chain. All eight stderr files are empty, all 18 boolean authority fields remain false, and only the final `evidence/2.authority_class` is authoritative. It names one exact formalization version, has no local producing run/job, supersession, or stale state, and records the protected actor/timestamp. This completes issue #21 but creates no source-claim truth status.
 
+Remote derived-status evidence: PR #39 merged final reviewed head `849dce08a84f70c7f4e1a00feb78aa863752b00f` as `8e65549d40b443497651b7dced2dc72d1b31335e`, tree `ca25e370a0ea5aa0312cef1e66720945a760da6b`. Exact-head PR run `29856409555` and main run `29856660451` passed all five required jobs. Protected publication run `29856660579`, job `88722566681`, retained the authority-only and post-fidelity CLI reads. Artifact `8505590232` contains 78 files and has GitHub and independently downloaded archive SHA-256 `e10111c9630b33e022d73ef45f716d958eb63491024b787a59e3949898be982f`.
+
+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 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.