Repository navigation
Pilot A: protected refutation and derived disproved status #41
Description
Goal
Complete the first real Pilot A path through MathOS's existing protected interfaces for the false source claim “Every prime number is odd.” The protected candidate must retain an exact witness 2, publish only a kernel-checked refutation of the claim's logical negation formalization, and derive disproved only after a separate v2 fidelity review.
This issue advances Pilot A steps 1–6 and the Phase 3 authoritative-refutation criterion. It does not claim completion of Pilot A or MathOS 1.0.
Required behavior
- Ingest the exact source statement through
mcl source create. - Normalize it as a universal claim over natural numbers through
mcl claim create. - Retain a no-import Lean 4.32.0 module with:
- an explicit checked witness theorem that
2satisfies the committed prime predicate and is not odd; - a theorem whose exact type is the logical negation of the normalized universal claim;
- no axioms or forbidden source tokens.
- an explicit checked witness theorem that
- Create the formalization with immutable
claim_polarity: negationand the exact theorem type/declaration identity. - Run the real local elaboration and audit services, then prepare
publication_request/1withoutcome: refutation. - Rebuild, dependency-check, and axiom-audit the exact module in the protected publication workflow.
- Preserve the existing attestation, staging, controlled ingestion, receipt, and atomic authority boundary unchanged.
- Promote exactly one accepted authoritative
lean_kernel_refutationfor the exact formalization version; no caller-authored or workflow Boolean may grant authority. - Show
open/no_current_verified_fidelitybefore review. - Have the distinct
protected-fidelity-reviewersubmit a closed v2 review oflogical_negationagainst the exact source/claim/formalization chain. - Derive
disprovedwith one exact refutation witness after review; never persist or accept a truth-status mutation. - Retain the before/after status, fidelity, authority, request/report/closure, Lean outputs, and attestation evidence in the workflow artifact.
- Keep the standalone non-authoritative
Trueisolation smoke intact.
Tests and adversarial checks
- The committed Pilot A module compiles with the pinned local Lean toolchain and
#print axiomsreports no axioms. - Existing publication outcome/polarity mismatch checks continue to reject a proof request for a negation formalization.
- Existing altered/missing closure, CAS, attestation, currentness, role-separation, and fidelity-relation checks remain green.
bash -npasses for publication scripts.- Formatting, warnings-denied Clippy, all Rust tests, legacy Python regressions, and
git diff --checkpass. - PR exact-head Linux, Windows, Lean, storage, and legacy jobs pass.
- Protected post-merge publication passes and its downloaded artifact is independently audited for exact hashes, closure membership, refutation authority, fidelity relation, and derived status.
Documentation
- Update the implementation status and release checklist with only evidence actually produced.
- Update publication-boundary documentation to distinguish the retained standalone
Truesmoke, historical proof authority, and the current Pilot A refutation candidate. - Record exact PR-head and post-merge run, commit, tree, artifact, and semantic identities in GitHub and the implementation ledger.
Non-goals
- Counterexample-package schema and API.
- Atomic repaired-claim creation and
research.repairsedge. - Proof of the repaired claim.
- Pedagogy generation, release export, RL export, the remaining pilots, or the 1.0 acceptance command.
Activity
Mnehmos commentedon Jul 21, 2026
Implementation candidate published as PR #42.
Exact head
1a5755fa815ca187c594e1d4db0c488d0a5e327c, tree8945fd4746c1f9d9d536dd14d17854da3c9d0bdd.Local evidence is green: pinned Lean compiles the exact no-import module; a real Windows
mclCLI playtest completed source → universal claim → negation formalization → elaboration → axiom-free audit →refutationrequest; selectingprooffor the same formalization failedMCL_PUBLICATION_OUTCOME_MISMATCH. Formatting, warnings-denied Clippy, 148 Rust tests, real Lean integration, 39 legacy regressions, Bash syntax, Actionlint, and whitespace checks pass.Protected authority and derived
disprovedremain pending exact-head CI, merge, protected-main publication, and independent artifact audit.Mnehmos commentedon Jul 21, 2026
Protected merged-tree audit — passed
Canonical merge:
18abdd23025cc245f0b5722a8676e5b3f1bb22378945fd4746c1f9d9d536dd14d17854da3c9d0bdd29860589159— all five jobs passed29860588969, job88735987761— passed8507149183,publication-boundary-18abdd23025cc245f0b5722a8676e5b3f1bb22377172aa87bccedf6a694299d076e6279061cd541cf5d4b8625d01bb7e0ba3b87fIndependent replay matched all 78 ZIP members, parsed all 54 JSON files and 25 JSONL closure entries, and rehashed every fixed role. All eight stderr files are empty. The retained module exactly matches the committed LF-normalized Git blob, has SHA-256
1e011925f7444a635c263725bf5f7dfc6fabdcd17c6f7e97135b22a534cc5af3, declares no imports, retainstwo_is_prime_and_not_odd, and both local/protected axiom outputs report no axioms.Exact lineage:
019f861a-16f5-7891-a15e-d86bb82cb6f3/89410bfeab715c5045558e7e628de8c860a3b0bb262151d9ddc5bcd4e232b61c019f861a-1706-7981-9f4f-0ed1231ef72c/739c66af9a18a882b5c988bb3f4eb658c87c24a4a0e2f559572b39448a67d1a7019f861a-171a-7b22-abe8-45cd917bc797/1f9621d15a83cbf3c201cd6d3cc739f4624cee59fdc103cf603b94f86ebac0b9513ed6ddb73294d03e8225298ef1f94b123434b52fa65da3540ead4a8ca88e7d0ab1aa3c7e46814b06d235987caa0b0fae7cf146ff717697ceafcb8ff625a10685a72971c8715c7998492143a0e63db18fae06da7283d1d8be313c66d036f3402f82f4c28c76736ce65597608f33b9ddf719a6bc4dc213e80b92c8008b5aca9f1ec7bbd2054173bba8cb310e66fbfc7dcff47171416ffd80ce0b02034197461d089af2f16be942bbb58995df745165ce4bba2f4a6273fd7955446974484045df46d88e197a040be6ce851fb28f980aee1f4dfda7714e304e5dd6e807405aaa52Authority evidence
019f861a-4b93-7a11-98e7-9e39aaa18192/52484265b0cae459cca257b95cbec4f00033987929ff7394b3db3ffa547d9225is exactlylean_kernel_refutation/accepted/authoritative, bound to the formalization and full receipt closure. Before fidelity, status isopen/no_current_verified_fidelity. Distinct reviewerprotected-fidelity-reviewerthen records v2logical_negationrequest1bedad0a3f33b69b913c4979c52f9ca202781646c3f11f2f54a448872de61af5, reportb0a7b0f297ac397b47422cb14680ce7dcb0d42dcd7090d76259967b4b4c49872, and evidence019f861a-4c13-7932-9257-83c145aa28eb/8d809395a76a5c23b126053d6b70e40a398d346a876b821ee25d9cbcf2119bfc. The second read isdisprovedwith one exact refutation witness.The attestation binds the exact protected workflow, commit, ref, run, GitHub-hosted runner, repository ID
1305399818, owner ID193347153, report digest, and Rekor timestamp2026-07-21T19:14:47Z. No retained Boolean saysauthoritative:true; exactly oneauthority_classis authoritative.Issue #41 is complete. Pilot A remains incomplete: counterexample packaging, immutable repair, repaired proof, pedagogy, release, and RL export are still open.
Mnehmos commentedon Jul 21, 2026
Evidence-ledger follow-up: PR #43 merged as
364bad572cfd362e41492a6eded2250ee4ecbefb. Post-merge CI run29861826124and protected publication run29861826102passed; artifact8507636126independently reproduces the refutation-authority, logical-negation fidelity, andopen -> disprovedderivation on the ledger merge. The exact proof/refutation evidence checklist item is now recorded as satisfied. Pilot A itself remains open at counterexample packaging, immutable repair, repaired proof, pedagogy, and export.