Mnehmos · Jul 21, 2026 · Jul 21, 2026
@@ -0,0 +1,11 @@
+# The Smallest Exception
+
+Author: GPT-5.6 Sol
+
+“Every prime number is odd” has the shape of a law and the lifespan of a glance. Two is enough to end it.
+
+That smallness is useful. A counterexample does not need to overpower a universal claim; it only needs to be exactly where the claim said it could not be. The force comes from fit, not size. A system for mathematics should remember that distinction. Search may suggest the witness, but the witness becomes consequential only when its definitions, computation, and relation to the original sentence survive inspection.
+
+There is also a temptation to repair the sentence while disproving it—to hear “except two” so quickly that the failed claim disappears. MathOS must resist that kindness. The false statement deserves its own durable identity and history. Its repair will be a new object connected by an explicit edge, not an erasure that makes the past look cleaner than it was.
+
+For now, two crosses only the first boundary. It is retained in a proof term, checked without axioms, and carried toward protected refutation. Explanation, repair, and teaching come next. The trace should make each transformation visible, because mathematical understanding is often the art of learning exactly which change made a statement true.
@@ -29,6 +29,8 @@ 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.
+
 ## Verification
 
 - [x] Lean verification uses pinned environments.

@@ -209,12 +209,14 @@ These items establish only part of the product foundation and trace model. One e
 - PR #39 merged its final reviewed head `849dce08a84f70c7f4e1a00feb78aa863752b00f` as `8e65549d40b443497651b7dced2dc72d1b31335e`, tree `ca25e370a0ea5aa0312cef1e66720945a760da6b`. Exact-head PR run `29856409555` and post-merge main run `29856660451` passed Rust on Ubuntu and Windows, real storage, legacy Python, and pinned Lean. Protected publication run `29856660579`, job `88722566681`, passed candidate construction, attestation, controlled ingestion, authority promotion, role-separated fidelity review, both CLI status reads, and retention.
 - Artifact `8505590232`, `publication-boundary-8e65549d40b443497651b7dced2dc72d1b31335e`, is 88,165 archive bytes with GitHub and independently downloaded SHA-256 `e10111c9630b33e022d73ef45f716d958eb63491024b787a59e3949898be982f`. Its 78 files expand to 144,589 bytes. Independent replay parsed all 54 JSON files plus 25 JSONL closure entries, matched every ZIP member, and recomputed the publication report (`6fdd7982316e28be2dd7a69b2ec743a37cae5479807e77ee00db749e9499b09b`), 25-role closure (`4e2acef7c87d19421e0305eb1dcfbd7cf5bc6e701528bd815799cc008fc8a7bb`), stage (`6036e9c90cf8edc550e898912bdd2a8672e3b76cd4ba6ba31318e5f9378dc2e5`), receipt (`61b804b1888f71346e15e6e96452af58a34703507cdbf9d637834b0272ae1cf1`), candidate bundle (`27fbff08373c79d348b85495ba7e6c821386060bfb4c8f247cce3ab83528e217`), and raw verifier output (`fca79f52d98c047dde52f49c6d0e417506c30b27bccfe97ffdb316204fa0391e`). The signed subject, protected workflow, repository and owner IDs, exact commit/ref/run, GitHub-hosted runner, and single Rekor timestamp `2026-07-21T18:19:58Z` all match.
 - The retained exact claim `9ec518612be9eeb8c7ac4f9ace5716f746f82dbc2864f8074227533d7994eae3` first returns `open/no_current_verified_fidelity` despite accepted authoritative proof evidence `529d361b5a4b1920579498cc5eeb8e78fb3a6567b46766a498f911d6f9308380`. A separate `protected-fidelity-reviewer`, distinct from formalization author `publication-candidate`, then records v2 `claim` fidelity request `b12e35aca5c921e5af0cc8b1f6b7aebff3b20f2cc0467cb79ee89961ca554785`, report `c0a74cda75ab6e919c3b216a4d0b247bd3bd7133c088293827ec034490ae0708`, and reviewed evidence `afb6304b0af81b8dc18a51d41636519b5276e30ce73fdff2eb57c3af5eb5bdb3`; the same read then returns `proved` with one exact witness. No retained Boolean says `authoritative:true`; exactly one accepted `evidence/2.authority_class` is authoritative.
+- Issue #41 changes only the canonical protected candidate, not the trust boundary. `fixtures/publication/PilotARefutation.lean` defines the natural-number predicates `Prime n := n >= 2` with no divisor from `2` through `n - 1`, and `Odd n := n % 2 = 1`; proves the explicit witness `two_is_prime_and_not_odd`; and proves `MathOS.PilotA.every_prime_is_odd_refuted`, whose exact type is the logical negation of the normalized Pilot A source claim. It needs no imports, compiles under pinned Lean 4.32.0, and reports no axioms. The producer now creates the exact source statement, universal natural-number claim, negation-polarity formalization, and `refutation` request through the existing CLI before the unchanged protected boundary. The standalone `True` isolation smoke and historical proof evidence remain intact.
+- A real Windows CLI playtest on Lean 4.32.0 created source `019f8611-2e62-7a83-9cbd-1cbe9f99fc6f` / `cca3b3bf790efb6490ac7cc38cebc5775b4e00281d7e32b7363ff44b5d23119b`, claim `019f8611-2e73-7063-b63d-c8f7fab2b950` / `12629132ce6e61eb470e3b3b69196690d6b9f862c8c89d88adc43ab2bb7da161`, and negation formalization `019f8611-2e83-70b2-96a2-1e26b2520385` / `a2299254827a7bd8d2b81ea73669094667ad1bc216367c142979e184aeac95a3` for module `1e011925f7444a635c263725bf5f7dfc6fabdcd17c6f7e97135b22a534cc5af3`. Real elaboration job `019f8611-2e94-7ef2-9e51-a292cc720f9c` and axiom-free audit job `019f8611-3113-7cf3-8dbb-31f6986a58fe` passed. Request `1fbee23ec5d537efb72fe5410bf314cfad90b76a16ec531a5937c5f546bc4a3d` preserved `refutation`; the same exact closure with caller-selected `proof` failed `MCL_PUBLICATION_OUTCOME_MISMATCH`. The local status remains non-authoritative `open/no_current_verified_fidelity`; protected refutation authority and `disproved` are not claimed before merged-tree evidence exists.
 
 ## Next highest-priority criteria
 
-1. Complete Pilot A through the real CLI/MCP application paths, including a protected refutation example if its false statement is formalized as negation.
-2. Implement the next unmet section 30 lifecycle criterion without weakening the derived-status trust boundary.
-3. Continue toward a replayed, portable release without treating Phase 3 status derivation as MathOS 1.0.
+1. Merge and independently audit issue #41's protected Pilot A refutation and derived `disproved` transition.
+2. Add the counterexample package and immutable repaired-claim path, then prove the repaired Pilot A claim.
+3. Continue Pilot A pedagogy/export and the remaining section 30 criteria without treating this partial path as MathOS 1.0.
 
 ## Exact last validation commands
 
@@ -241,6 +243,7 @@ Observed validation evidence for this update:
 - Issue #38 validation passes warnings-denied Clippy, 148 Rust tests across workspace/all targets, real Lean 4.32.0 integration, all 39 legacy Python regressions, Bash syntax, Actionlint 1.7.12, formatting, and patch whitespace checks. Proof and refutation application fixtures cover every supported terminal and nonterminal derivation plus concurrency, currentness, corruption, and restart failures; CLI and MCP adversarial tests reject status, evidence, formalization, actor, idempotency, and dry-run selectors.
 - A review-found moved-source flaw was repaired before merge: a tombstoned or non-current source head now invalidates the former witness as `open/source_version_not_current`, and a full authority-plus-fidelity regression fixture proves it. The final fidelity v2 report-variant parser test also passes on exact PR head `849dce08a84f70c7f4e1a00feb78aa863752b00f`.
 - Post-merge main CI run `29856660451` and protected publication run `29856660579` both pass on `8e65549d40b443497651b7dced2dc72d1b31335e`. The independently downloaded 78-file artifact passes the exact byte, schema, closure, receipt, authority, status, and attestation audit recorded above.
+- Issue #41 local playtest compiled module `1e011925f7444a635c263725bf5f7dfc6fabdcd17c6f7e97135b22a534cc5af3` with pinned Windows Lean 4.32.0, completed the real CLI source/claim/negation-formalization/elaboration/audit/request path, observed no axioms, prepared refutation request `1fbee23ec5d537efb72fe5410bf314cfad90b76a16ec531a5937c5f546bc4a3d`, and rejected the mismatched proof request as `MCL_PUBLICATION_OUTCOME_MISMATCH`. Bash syntax and patch whitespace checks pass. Protected evidence remains pending.
 - Before the review-driven immutable GitHub ID pin changed the publication policy hash, a real Windows CLI playtest staged protected run `29716676599`'s exact report (`12f0aaca0f6e9a16c242205da24f53fadc08ba9177cff6e039ec394c50ee1012`), bundle (`a23d190fdaffe7e87fc98747b32525f96f199aa05f5431cba39548b38207a84e`), and all 25 retained roles as stage `65569142db500d44480ab879d4799d6103450c584e90d923ecc881a55e013d2d`. Dry-run created no stage, exact retry output was byte-stable, missing and altered report CAS bytes failed as `MCL_PUBLICATION_STAGE_MEMBER_MISSING` and `MCL_PUBLICATION_STAGE_MEMBER_MISMATCH`, restored `doctor` was healthy, and fresh-store ingestion failed `MCL_RECORD_NOT_FOUND` rather than importing caller snapshots or reaching the platform-pinned verifier. The stronger committed policy intentionally makes that historic candidate stale; merged current-policy evidence is now recorded above.
 - 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.

@@ -60,7 +60,9 @@ The commit and tree values in this local request are proposed source identities.
 
 ### Protected candidate and retained closure
 
-The protected workflow refuses to start unless GitHub's immutable run context reports that `main` is actively protected. It then constructs one fresh, real canonical lifecycle for the no-import `MathOS.Publication.smoke` declaration, prepares its request through the same application service, and rebuilds the exact retained module twice inside Bubblewrap: once for elaboration and once with a verifier-controlled `#print axioms` driver. Both subprocesses use a read-only root, separate mount, PID, and network namespaces, one Lean worker thread, a 120-second timeout, a four-gibibyte Lean heap cap, and a six-gibibyte process address-space ceiling for runtime and thread overhead.
+The protected workflow refuses to start unless GitHub's immutable run context reports that `main` is actively protected. It then constructs one fresh, real canonical lifecycle for the no-import Pilot A declaration `MathOS.PilotA.every_prime_is_odd_refuted`, prepares a refutation request through the same application service, and rebuilds the exact retained module twice inside Bubblewrap: once for elaboration and once with a verifier-controlled `#print axioms` driver. The retained module defines the exact natural-number prime and odd predicates, proves the explicit witness `2` is prime and not odd, and uses that witness to prove the logical negation of “Every prime number is odd.” Both subprocesses use a read-only root, separate mount, PID, and network namespaces, one Lean worker thread, a 120-second timeout, a four-gibibyte Lean heap cap, and a six-gibibyte process address-space ceiling for runtime and thread overhead.
+
+The earlier `MathOS.Publication.smoke : True` module remains the standalone non-authoritative isolation smoke. Historical protected artifacts also retain an independently audited authoritative proof for that declaration. Changing the canonical candidate to Pilot A does not reinterpret or overwrite that evidence: the new source, claim, negation-polarity formalization, request, receipt, and refutation evidence all receive new immutable identities.
 
 The request-bound environment remains truthfully marked `local` because it describes the diagnostic and audit evidence created by the ordinary worker. Its manifest contains the exact Lean toolchain, no dependencies, no imports, and the checked-in `lean-toolchain` hash. The candidate report separately records the stronger GitHub-hosted runner, clean checkout, dependency closure, network isolation, and memory controls actually observed by the protected workflow. A local trust-profile label is never upgraded in place.
 
@@ -160,10 +162,8 @@ Formalization authority and statement fidelity remain deliberately separate. Thi
 
 ## Current implementation state
 
-The closed policy, request, retained-closure, candidate-report, quarantine-stage, attestation-verification, authority-binding, and authoritative-evidence contracts are implemented. The shared application, CLI, and MCP request-preparation paths derive and retain a non-authoritative request from exact current local evidence without accepting caller-authored JSON. The protected `main` workflow retains the earlier boundary smoke and additionally produces, application-validates, attests, independently challenges, stages, ingests, promotes, and retains a real `publication_report/1`, its complete exact closure, raw verifier output, canonical CAS attestation-verification record, separate immutable non-authoritative SQLite ingestion receipt, and receipt-bound authoritative evidence. Pull-request CI exercises the same candidate producer and quarantine persistence, but its deliberately synthetic bundle cannot cross the ingestion or authority boundary.
-
-That workflow capability is now observed on merge `95bd8a1d2068612b5eca644c3d77754b5e4f49fd`. Protected run `29721420136` retained artifact `8452528096`; downloaded inspection recomputed the exact report, 25-role closure, candidate bundle, quarantine stage, raw verifier output, and canonical attestation-verification/receipt hashes. The closed result binds immutable repository ID `1305399818`, owner ID `193347153`, the protected workflow, `main`, merge commit, run and attempt, one report subject, one source dependency, GitHub-hosted execution, and Rekor timestamp `2026-07-20T06:22:33Z`. Every retained authority field remains false.
+The closed policy, request, retained-closure, candidate-report, quarantine-stage, attestation-verification, authority-binding, authoritative-evidence, polarity-aware fidelity, and derived-status contracts are implemented. The shared application, CLI, and MCP request-preparation paths derive and retain a non-authoritative request from exact current local evidence without accepting caller-authored JSON. The protected `main` workflow retains the standalone boundary smoke and additionally produces, application-validates, attests, independently challenges, stages, ingests, promotes, and retains a real `publication_report/1`, its complete exact closure, raw verifier output, canonical CAS attestation-verification record, separate immutable non-authoritative SQLite ingestion receipt, receipt-bound authoritative evidence, role-separated fidelity review, and before/after derived-status reads. Pull-request CI exercises the same candidate producer and quarantine persistence, but its deliberately synthetic bundle cannot cross the ingestion or authority boundary.
 
-The attestation-verification record and SQLite ingestion receipt remain non-authoritative. Together they can establish that exact retained report bytes were signed by the constrained protected workflow and witnessed by the configured transparency system. The implemented atomic gate is the only path that can turn that fully replayed closure into authoritative evidence.
+Historical protected proof authority is observed and independently audited on merge `0ef8a132dfb99e63238325ac035de948e893f791`, run `29726693055`, artifact `8454565233`. Derived source-claim status is observed and independently audited on merge `8e65549d40b443497651b7dced2dc72d1b31335e`, run `29856660579`, artifact `8505590232`: authority alone leaves the source claim open, and a distinct reviewer’s v2 `claim` fidelity evidence changes the derived read to `proved` without persisting a verdict.
 
-No protected merged-tree authority promotion has yet been observed for this implementation candidate. No mathematical claim status is derived.
+The attestation-verification record and SQLite ingestion receipt remain non-authoritative. Together they can establish that exact retained report bytes were signed by the constrained protected workflow and witnessed by the configured transparency system. The implemented atomic gate is the only path that can turn that fully replayed closure into authoritative evidence. Pilot A refutation authority and the resulting `disproved` status remain pending until the exact changed producer is merged, run on protected `main`, and independently audited.
@@ -0,0 +1,18 @@
+namespace MathOS.PilotA
+
+def Prime (n : Nat) : Prop :=
+  n >= 2 ∧ ∀ d : Fin (n + 1), d.val >= 2 -> d.val < n -> n % d.val ≠ 0
+
+def Odd (n : Nat) : Prop :=
+  n % 2 = 1
+
+theorem two_is_prime_and_not_odd : Prime 2 ∧ ¬ Odd 2 := by
+  unfold Prime Odd
+  decide
+
+theorem every_prime_is_odd_refuted :
+    Not (∀ n : Nat, MathOS.PilotA.Prime n -> MathOS.PilotA.Odd n) := by
+  intro universal_claim
+  exact two_is_prime_and_not_odd.2 (universal_claim 2 two_is_prime_and_not_odd.1)
+
+end MathOS.PilotA