Mnehmos · Jul 20, 2026 · Jul 20, 2026 · Jul 20, 2026
@@ -33,7 +33,7 @@ Remote fidelity evidence: GitHub Actions run `29706138708` passed fresh Linux, W
 - [ ] Authoritative proof and refutation evidence is recorded against exact formalization versions.
 - [ ] Hole, unsafe, and axiom policies are enforced.
 - [ ] Replay works and reports its exact trust boundary.
-- [ ] Publication CI produces retained evidence.
+- [x] Publication CI produces retained evidence.
 
 Phase 1 evidence: `lean-toolchain` pins Lean 4.32.0. No proof-authority item is complete.
 
@@ -49,11 +49,13 @@ Phase 3 diagnostic evidence: the closed `evidence/1` contract names exact subjec
 
 Phase 3 local audit evidence: the committed audit policy and closed request/report schemas bind an exact formalization, accepted elaboration diagnostic, environment, module, declaration, and policy identity. Durable audit jobs run source escape scans and verifier-controlled `#print axioms`, retain private diagnostics, and atomically promote diagnostic proof-closure and axiom-audit evidence. Policy mismatch, malformed output, duplicate axioms, retries, restart, partial promotion, and corruption fail closed. Local audits explicitly lack publication memory and network isolation and cannot become authoritative, so the complete proof-authority and publication criteria remain unchecked.
 
-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 replay 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; polarity remains intent until combined with reviewed fidelity. Merged-tree ingestion evidence and authoritative evidence creation remain incomplete, so every proof-authority criterion remains unchecked.
+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 replay 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; polarity remains intent until combined with reviewed fidelity. Merged-tree controlled-ingestion evidence is complete and recorded below. Authoritative evidence creation remains incomplete, so every proof-authority criterion remains unchecked.
 
-Remote evidence: GitHub Actions run `29704542965` passed the exact real Lean audit lifecycle and fresh Linux and Windows suites on tree `30d55d6e2ce7b0de2d921cff3e1368124fd9f66f`. This validates the local diagnostic audit capability only. The verification checklist remains open until publication-profile authority, replay, and retained publication evidence are complete.
+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.
 
-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. The first real protected candidate run for the retained-closure slice is still pending its merged tree.
+Remote evidence: GitHub Actions run `29704542965` passed the exact real Lean audit lifecycle and fresh Linux and Windows suites on tree `30d55d6e2ce7b0de2d921cff3e1368124fd9f66f`. This validates the local diagnostic audit capability only. The remaining verification checklist items stay open until publication-profile authority and replay are complete.
+
+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.
 
 Repository protection evidence: live GitHub API reads now report `main` as protected. Pull requests, strict passage of the five CI jobs, resolved conversations, stale-review dismissal, and admin enforcement are required; force-pushes and deletions are disabled. The protected candidate also checks GitHub's immutable protected-ref context at runtime. This administrative control does not itself grant proof authority.