Repository navigation
Pilot A: atomic counterexample package and immutable claim repair #44
Description
Context
Pilot A has an independently audited exact refutation and derived disproved result in #41 / PR #42. PR #43 records that evidence. The next required behavior in SPEC sections 11.4, 14.3–14.4, and 29.1 is to preserve the false claim, package witness 2, and create a distinct repaired claim excluding 2.
This issue is the next focused slice from #25. It does not prove the repaired claim or complete Pilot A.
Objective
Add one shared application capability that turns a currently derived refutation witness into a canonical counterexample package and a linked repaired claim, with one atomic logical commit and no mutation of the original claim or its derived status.
Required contract
- Add a closed, versioned
counterexample_package/1domain contract and committed JSON Schema. - The canonical package must contain:
- exact source and original claim versions;
- an exact canonical JSON witness plus mathematical type;
- exact refuted formalization;
- deterministic checker binding derived from that formalization;
- the current role-separated fidelity and receipt-bound authoritative refutation identities;
- optional minimization documentation and supporting artifact hashes;
- explanation of the failing assumption;
- the complete proposed repaired
claim/1payload and its canonical version hash; - exact counterexample-search run ID and event-head hash.
- The package must be canonical JSON in CAS with controlled artifact metadata. It is a package of already revalidated evidence, not a new authority assertion.
- Add a closed repair-operation enum covering SPEC section 14.4; Pilot A uses
exclude_boundary_case.
Application and atomicity
Add one application-only repair path. Callers may supply the original claim identity, select the refutation formalization, provide the exact witness/explanations/search-run identity, and propose a repaired claim payload. They may not supply status, authority, fidelity, receipt, checker, hashes, object IDs, edges, or package bytes.
The application must:
- rehash the exact source/claim/formalization records;
- replay the complete current fidelity and publication-authority chains through the existing derived-status path;
- require the current exact claim status to be
disprovedand the selected formalization to be a current refutation witness; - validate a
counterexample_searchrun, its complete event chain, and exact current head; - require the repaired claim to use the same exact source, differ canonically from the original, and pass
claim/1validation; - derive the checker/evidence/package fields and canonical hashes itself;
- stage package bytes in CAS, then use one immediate SQLite transaction to recheck the captured truth basis and run head, register the package artifact, create a new claim object, add one immutable
research.repairsedge from repaired claim to original claim, and write the idempotency result; - leave no logical partial state on any failure. Orphaned content-addressed bytes are non-semantic and may be garbage-collected later;
- keep exact retry byte/result stable and reject idempotency-key rebinding;
- leave the original claim/version/status/evidence untouched.
Generic edge creation must reject research.repairs; only the controlled repair path may create that edge shape.
Interfaces
- Expose repair and package retrieval through the CLI.
- Expose the same operations through MCP using the same application service.
- Do not add direct truth-status mutation, raw evidence creation, raw package ingestion, or caller-selected repair edges.
- Extend the protected Pilot A workflow to run the real CLI after the
disprovedread and retain the exact package, repaired claim, and repair edge.
Acceptance tests
- Closed-schema, unknown-field, canonical-byte, size, exact-reference, and hash tests.
- Dry-run returns proposed hashes but writes no artifact row, claim, edge, or idempotency receipt.
- Positive refutation fixture creates one package, one new claim object, and one repair edge atomically; retry and restart are identical.
- Original claim remains current and
disproved; repaired claim begins independently without inherited fidelity or proof. - Refuse open/proved/ambiguous/superseded claims, proof witnesses, unselected refutation witnesses, stale source/claim/formalization/fidelity/authority heads, missing/corrupt CAS, wrong or changed search run/head, invalid run chain, same-content “repair,” wrong source, malformed witness/package data, and idempotency rebinding.
- Transaction-failure injection proves no logical partial writes.
- Concurrent basis/head change loses with a retryable conflict.
- CLI and MCP adversarial tests reject caller-authored status/evidence/checker/hash/object/edge fields.
- Formatting, warnings-denied Clippy, all Rust tests, real pinned Lean integration, legacy Python, Bash syntax, Actionlint, and
git diff --checkpass. - Protected merged-tree evidence is downloaded and independently audited before closing.
Pilot A exact repair
Proposed new claim:
Every prime number other than 2 is odd.
The original claim “Every prime number is odd.” remains a separate immutable claim with derived status disproved.
Non-goals
- proving or publishing the repaired claim;
- pedagogy units or release/RL export;
- checking the broad counterexample/repair lifecycle or Pilot A checklist boxes before t 8CCE hose later slices pass.
Activity
Mnehmos commentedon Jul 21, 2026
Implementation is ready for exact-head review in #45.
Local head:
fec9db8398cd9851ca0e7eacbfe9a8bd8e2608b1Local verification passed:
cargo fmt --checkgit diff --checkThe issue remains open until the merged-tree protected publication artifact is downloaded and independently audited. Proving the repaired claim remains a later slice.
Mnehmos commentedon Jul 21, 2026
Protected merged-tree acceptance is complete.
Exact Git identities:
1e9066f01ed75ba30156718710d2451db4f7a4a8903811d22a4bcc1bff7b50ec06186a44d6a26fb6a255608aae1abf31bea27d6a11d26e08d18f0b22GitHub verification:
29866704074: all five jobs passed on the exact merge commit29866704122, job88756652960: passed protected-ref enforcement, contained Lean, both attestations/challenges, controlled ingestion/promotion, atomic counterexample repair, and retention8509521719,publication-boundary-1e9066f01ed75ba30156718710d2451db4f7a4a8, GitHub-reported archive size105742bytesIndependent downloaded-artifact audit:
refs/heads/main, GitHub-hosted execution, and run attempt 1counterexample_search_result/1event:7e6627025dc9ed2ccd91eeb0ae08205babedea1d6c6ee17832aec28e5c0a008c019f8669-618e-7291-a0e7-e161ceec44c0Natvalue214bff23f2e7afe79d2fec05fa5d4d89a0340151398529e322e7112fd7dc83652from its exact 2,944 bytes914f03a02ffba3a774fbcbb1c753c221593409d067fb07b5061b1a055e61eb55, fidelity691e7def809ee7c2e11fafb69a7dff1a5067f57e0b0b82bd1347db5f83336230, and receipt806f9a6e1cad16b76149c8cedac74b511100a40f8084ee1259abaa3e3c99ae90019f8669-1b1e-7c32-8280-2bcaf4aa01f4/f40843ae3c953ffd076d669ea878b7c0efad4e5fa92351114763b7e56460b237remained byte-identicallydisproved019f8669-622f-73c3-8ca7-cb5f15da829d/f7d4cdccc4e5be9d78991a5095d80b1eb7bf5a4e5ccffe8c1454d90377d2bb88is a distinct no-predecessorclaim/1and startsnot_started019f8669-6230-7c01-9011-26ad0e840f3dpoints from the repaired exact version to the original exact version withexclude_boundary_caseand the exact package/run/formalization bindingThis satisfies issue #44. It does not prove the repaired claim or complete Pilot A / MathOS 1.0. The next focused slice is a new formalization, protected proof authority, and role-separated fidelity for the repaired claim without changing the original claim or repair package.