Mnehmos · Jul 20, 2026 · Jul 20, 2026
@@ -49,7 +49,7 @@ 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, and candidate report 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. Candidate reports are structurally non-authoritative. ADR-0006 requires OIDC and Sigstore attestation verification before promotion. The actual clean-checkout workflow, attestation, verified ingestion, and authoritative evidence remain incomplete, so every proof-authority criterion remains unchecked.
+Phase 3 publication contract evidence: the closed publication policy, request, and candidate report 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. The application now derives canonical private request artifacts from the current formalization head and one exact accepted elaboration/audit chain, recomputes every retained local CAS object, and exposes the same non-authoritative operation through CLI and MCP 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. Transactional head and idempotency checks cover matching preexisting CAS identities. Retry, restart, stale subject, conflicting key reuse, missing/substituted evidence, corrupted evidence artifacts, and invalid or mismatched outcomes fail closed. Candidate reports are structurally non-authoritative. Polarity remains intent until combined with reviewed fidelity. ADR-0006 requires OIDC and Sigstore attestation verification before promotion. A real protected candidate closure, verified ingestion, and authoritative evidence remain 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.
 

@@ -169,6 +169,7 @@ These items establish only part of the product foundation and Phase 2 trace mode
 - Issue #20 is complete with exact-tree CI evidence. Issue #21 must now bind clean-checkout verification, dependency closure, retained artifacts, policy identity, and non-forgeable report provenance before authoritative proof or refutation evidence can exist.
 - The first issue #21 slice defines closed publication policy, request, and candidate-report contracts. The policy pins repository, protected workflow, main ref, GitHub-hosted runner, Lean toolchain, allowed axioms, required isolation controls, SLSA predicate, and action commit identities.
 - Publication requests separately name proof and refutation outcomes and bind exact diagnostic, proof-closure, axiom-audit, environment, module, declaration, policy, Git commit, and Git tree identities.
+- `mcl verify prepare-publication` and MCP `verify.prepare_publication` now derive that request from the current canonical formalization head and its exact accepted elaboration/audit chain. Typed `claim_polarity` maps `claim` to proof and `negation` to refutation; earlier records may omit it for read compatibility but cannot publish until versioned and reverified. The application reopens the controlled jobs and reports, verifies every referenced CAS object, and retains only private `generated` canonical request bytes behind a transactional head/idempotency check. Callers cannot submit request JSON, derived hashes, or authority fields, and polarity remains non-authoritative intent until fidelity and protected publication evidence are combined.
 - Candidate reports must remain non-authoritative. A passed candidate fails validation if clean checkout, dependency closure, network isolation, memory enforcement, allowed axioms, retained artifacts, workflow identity, source identity, or policy identity is missing or inconsistent.
 - ADR-0006 requires GitHub OIDC and Sigstore attestation of the exact report bytes, followed by repository, workflow, ref, commit, predicate, runner, and subject-digest verification before authority promotion. The policy now additionally pins GitHub CLI 2.96.0 by release archive and executable SHA-256.
 - The publication boundary smoke uses a clean checkout, pinned Lean, read-only root mount, separate mount, PID, and network namespaces, a private temporary filesystem, one Lean worker thread, and a four-gibibyte address-space limit. Its report remains explicitly non-authoritative.
@@ -182,7 +183,7 @@ These items establish only part of the product foundation and Phase 2 trace mode
 
 ## Next highest-priority criteria
 
-1. Implement controlled canonical ingestion for a real `publication_request/1`, `publication_report/1`, and complete retained publication closure.
+1. Feed the prepared canonical request into a real clean-checkout `publication_report/1` and complete retained publication closure.
 2. Create authoritative exact proof/refutation evidence only from the verified retained closure, never from caller-authored reports.
 3. Derive mathematical status only from exact current proof and fidelity evidence.
 4. Complete Pilot A through the real interfaces only after both authority and fidelity controls exist.
@@ -202,10 +203,10 @@ git diff --check
 Observed validation evidence for this update:
 
 - Home workstation: Windows 10.0.19045, PowerShell 5.1.19041.6456, Rust 1.97.1, Python 3.12.10, GitHub CLI 2.70.0, GNU Bash 5.2.21 through WSL, and Lean 4.32.0 `x86_64-w64-windows-gnu`.
-- `bash -n scripts/publication-attestation-verify.sh`, formatting, warnings-denied Clippy, all 89 default Rust tests, and patch whitespace validation passed.
+- Formatting, warnings-denied Clippy across all targets and features, all 92 default Rust tests, the opt-in real Lean 4.32 lifecycle, all 39 legacy Python regressions, and patch whitespace validation passed for the canonical request-preparation slice.
 - The corrected policy passed against retained artifact `8448611307`; independent report-digest, predicate, empty-timestamp, and empty-attestation mutations all failed closed.
 - `mcl init`, `mcl health`, and `mcl doctor` passed against a fresh Windows instance. Doctor observed the exact pinned Lean 4.32.0 toolchain and honestly reports the local profile.
-- The Windows legacy Python command preserved one failure because the installed Lean turns the test's assumed missing-toolchain result into a Lean rejection, plus two errors where SQLite connections opened directly by tampering tests remain locked during temporary-directory cleanup. The opt-in real Lean worker test also preserved a Windows `launch_failed` result. These host-specific failures remain open observations; they were not hidden or mixed into the attestation correction.
+- PR #29 corrected the Windows-specific Lean platform expectation and temporary-database cleanup assumptions. Main CI run `29709993224` and publication run `29709993225` passed after that repair.
 - PR #26 CI run `29709569292` passed fresh Linux, Windows, storage, legacy Python, and pinned Lean jobs on exact tree `e5b0bcbf4eacf9cb402d87b04b5dc9b0431134f2`.
 - GitHub Actions run `29699563931` passed all five jobs for the completed MCP invalid-action and environment-persistence state, including exact pinned Lean availability and both Rust operating-system targets.
 - GitHub Actions run `29700398370` passed all five jobs for the canonical artifact slice, including both Rust operating-system targets.

@@ -30,6 +30,34 @@ authoritative = false
 
 A report that says otherwise is invalid.
 
+### Request preparation
+
+The safe local preparation surface is:
+
+```text
+mcl verify prepare-publication \
+  --formalization-object-id <uuidv7> \
+  --formalization-version-hash <sha256> \
+  --outcome proof \
+  --diagnostic-evidence-id <uuidv7> \
+  --proof-closure-evidence-id <uuidv7> \
+  --axiom-audit-evidence-id <uuidv7> \
+  --source-commit-sha <git-sha1> \
+  --source-tree-sha <git-sha1> \
+  --actor <identity> \
+  --idempotency-key <stable-key>
+```
+
+Use `--outcome refutation` for a refutation request and `--dry-run` to validate without writing. MCP exposes the same application operation as `verify.prepare_publication`.
+
+The caller selects exact IDs and publication intent but cannot submit request JSON, evidence hashes, environment, module, declaration, policy, report, or authority fields. A publishable formalization must carry typed `claim_polarity`: `claim` binds a proof request and `negation` binds a refutation request. Omitting this field remains valid only for compatibility with earlier `formalization/1` records; publication preparation then fails closed, so a legacy formalization must be versioned and fully reverified. Changing polarity changes the formalization version identity and invalidates the old evidence chain.
+
+The application requires the current formalization head; rereads immutable diagnostic and audit evidence; verifies that the accepted audit pair came from one job and audited the selected elaboration diagnostic; reopens the controlled job reports; recomputes every referenced CAS object; and derives the remaining request fields from canonical state. A Store transaction rechecks the current head while recording the request and its idempotency receipt, including when identical request bytes already exist. The canonical bytes are retained as a private `generated` JSON artifact whose SHA-256 equals the request hash.
+
+`claim_polarity` is exact canonical intent, not proof that the Lean theorem faithfully represents the claim or its negation. Later authority creation must combine it with current reviewed statement-fidelity evidence and the protected publication closure; it must never infer authoritative proof/refutation kind from the label alone.
+
+The commit and tree values in this local request are proposed source identities. The protected clean-checkout workflow must derive and match the actual runtime commit and tree before producing a candidate. A prepared request is not evidence, is not a publication report, and grants no authority.
+
 ## Attestation stage
 
 The protected workflow attests the exact candidate report digest using GitHub OIDC and Sigstore. Authority ingestion must verify at least:
@@ -46,7 +74,7 @@ MathOS must parse the verifier output and match it to the report and committed p
 
 ## Current implementation state
 
-The closed policy, request, candidate-report, and attestation-verification contracts are implemented. A clean-checkout boundary smoke now runs a pinned trivial Lean theorem with one Lean worker thread inside Linux mount, PID, and network namespaces with a four-gibibyte address-space limit. The protected `main` workflow attests the exact smoke-report bytes, challenges that bundle with the independently pinned GitHub CLI verifier, and retains the report, raw verification result, constrained verification record, diagnostics, and Sigstore bundle. Pull-request CI exercises the isolation script without granting authority.
+The closed policy, request, candidate-report, and attestation-verification contracts are implemented. The shared application, CLI, and MCP paths can now derive and retain a non-authoritative publication request from exact current local evidence without accepting caller-authored JSON. A clean-checkout boundary smoke runs a pinned trivial Lean theorem with one Lean worker thread inside Linux mount, PID, and network namespaces with a four-gibibyte address-space limit. The protected `main` workflow attests the exact smoke-report bytes, challenges that bundle with the independently pinned GitHub CLI verifier, and retains the report, raw verification result, constrained verification record, diagnostics, and Sigstore bundle. Pull-request CI exercises the isolation script without granting authority.
 
 The attestation-verification record is still non-authoritative. It can establish that exact retained bytes were signed by the constrained protected workflow and witnessed by the configured transparency system. Canonical proof authority additionally requires a real `publication_report/1`, complete exact evidence closure, controlled ingestion, and a new authoritative evidence record produced by the application rather than accepted from caller JSON.
 

@@ -16,6 +16,7 @@
       }
     },
     "formal_system": {"enum": ["lean4"]},
+    "claim_polarity": {"enum": ["claim", "negation"]},
     "environment_hash": {"type": "string", "pattern": "^[0-9a-f]{64}$"},
     "module_artifact_hash": {"type": "string", "pattern": "^[0-9a-f]{64}$"},
     "declaration_name": {"type": "string", "minLength": 1, "maxLength": 1048576},