8000 Pilot A: publish protected prime-parity refutation by Mnehmos · Pull Request #42 · Mnehmos/MathOS · GitHub
[go: up one dir, main page]
Skip to content

Pilot A: publish protected prime-parity refutation - #42

Merged
Mnehmos merged 1 commit into
mainfrom
feat/pilot-a-protected-refutation
Jul 21, 2026
Merged

Pilot A: publish protected prime-parity refutation#42
Mnehmos merged 1 commit into
mainfrom
feat/pilot-a-protected-refutation

Conversation

@Mnehmos
@Mnehmos Mnehmos commented Jul 21, 2026
Copy link
Copy Markdown
Owner

Outcome

Advances Pilot A through the existing protected publication path for the false claim “Every prime number is odd.” The canonical candidate now retains witness 2, publishes a negation-polarity refutation request, and lets the unchanged protected ingestion/fidelity/status path derive disproved only after role-separated review.

Closes #41

Changes

  • add the no-import Lean 4.32.0 PilotARefutation.lean fixture;
  • define exact natural-number Prime and Odd predicates;
  • prove the named witness two_is_prime_and_not_odd and the universal claim's logical negation;
  • create the exact source, universal claim, negation formalization, and refutation publication request through mcl;
  • preserve the standalone non-authoritative True isolation smoke and historical proof evidence;
  • document the trust distinction, local evidence, open follow-on work, and build diary entry.

No publication, evidence, fidelity, or status schema/API changed. Counterexample packaging, claim repair, repaired proof, pedagogy, and export remain out of scope.

Local verification

Exact head: 1a5755fa815ca187c594e1d4db0c488d0a5e327c

Exact tree: 8945fd4746c1f9d9d536dd14d17854da3c9d0bdd

  • lean fixtures/publication/PilotARefutation.lean
  • real mcl CLI playtest: source → claim → negation formalization → elaboration → axiom-free audit → refutation request
  • mismatched proof request rejected as MCL_PUBLICATION_OUTCOME_MISMATCH
  • cargo fmt --check
  • cargo clippy --workspace --all-targets --all-features -- -D warnings
  • cargo test --workspace --all-targets — 148 passed
  • opt-in real Lean worker integration — passed
  • legacy Python regressions — 39 passed
  • Bash syntax for all publication scripts — passed
  • Actionlint 1.7.12 — passed
  • git diff --check

Merge gate

Do not merge until the exact PR head passes all five required jobs and review is clear. After merge, independently audit the protected publication artifact before checking the proof/refutation or Pilot A release criteria.

@coderabbitai
coderabbitai Bot commented Jul 21, 2026 •
edited
Loading
Copy link
Copy Markdown

Warning

Review limit reached

@Mnehmos, you've reached your PR review limit, so we couldn't start this review.

Next review available in: 53 minutes

Enable usage-based reviews in Billing to review now. Otherwise, wait until the next included review is available.
You're only billed for reviews past your plan's rate limits ($0.25/file).

How can I continue?

After more reviews become available, a review can be triggered using the @coderabbitai review command as a PR comment. Alternatively, push new commits to this PR.

To avoid repeated limits, reduce automatic review volume by pausing incremental auto-reviews earlier, using label-based review opt-in, excluding WIP or generated PR titles, or requesting reviews manually when the PR is ready. If your team needs uninterrupted high-volume reviews, an organization admin can enable usage-based reviews.

How do review limits work?

CodeRabbit enforces per-developer PR review limits for each organization. Most developers receive the normal plan review availability.

For paid Pro and Pro+ PR reviews, CodeRabbit uses adaptive limits for sustained high-volume activity. When a developer's recent PR review activity reaches the 95th percentile or higher among CodeRabbit users, additional reviews become available more gradually as earlier reviews age out of the rolling window.

Please refer docs for additional details.

Review details
⚙️ Run configuration

Configuration used: defaults

Review profile: CHILL

Plan: Pro

Run ID: 5c353d4c-abe2-4a54-9595-2818a686ef90

📥 Commits

Reviewing files that changed from the base of the PR and between f79d4bf and 1a5755f.

📒 Files selected for processing (6)
  • docs/dev-diary/0018-the-smallest-exception.md
  • docs/implementation/RELEASE_CHECKLIST.md
  • docs/implementation/STATUS.md
  • docs/trust/PUBLICATION_AUTHORITY.md
  • fixtures/publication/PilotARefutation.lean
  • scripts/publication-candidate.sh
✨ Finishing Touches
🧪 Generate unit tests (beta)
  • Create PR with unit tests
  • Commit unit tests in branch feat/pilot-a-protected-refutation

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

❤️ Share

Comment @coderabbitai help to get the list of available commands.

@Mnehmos Mnehmos mentioned this pull request Jul 21, 2026
Closed
@Mnehmos
Mnehmos marked this pull request as ready for review July 21, 2026 19:10
@Mnehmos
Mnehmos commented Jul 21, 2026
Copy link
Copy Markdown
Owner Author

Exact-head merge audit:

  • head 1a5755fa815ca187c594e1d4db0c488d0a5e327c
  • tree 8945fd4746c1f9d9d536dd14d17854da3c9d0bdd
  • CI run 29860329570 passed all five required jobs
  • pinned-Lean job 88735115671 passed the real contained worker, standalone smoke, full simulated Pilot A candidate, and staged-CAS barrier
  • GraphQL thread audit found zero review threads and zero submitted reviews
  • CodeRabbit reported success but explicitly skipped review because of its rate limit; no automated findings exist
  • branch protection reports strict exact-head checks, conversation resolution, admin enforcement, and zero required approvals

Manual diff review found no authority-boundary or scope expansion: the change supplies a new exact no-import fixture and selects existing refutation/polarity paths. The release and Pilot A checkboxes remain open pending protected post-merge evidence and later repair/pedagogy/export work.

@Mnehmos
Mnehmos merged commit 18abdd2 into main Jul 21, 2026
6 checks passed
@Mnehmos
Mnehmos commented Jul 21, 2026
Copy link
Copy Markdown
Owner Author

Post-merge evidence: main commit 18abdd23025cc245f0b5722a8676e5b3f1bb2237, tree 8945fd4746c1f9d9d536dd14d17854da3c9d0bdd; CI 29860589159 and protected publication 29860588969 passed. Artifact 8507149183 independently hashes to 7172aa87bccedf6a694299d076e6279061cd541cf5d4b8625d01bb7e0ba3b87f and passes exact 78-file/25-role replay. Authority evidence 52484265b0cae459cca257b95cbec4f00033987929ff7394b3db3ffa547d9225 is accepted authoritative lean_kernel_refutation. Status is open/no_current_verified_fidelity before the distinct review and disproved with one refutation witness after v2 logical_negation fidelity evidence 8d809395a76a5c23b126053d6b70e40a398d346a876b821ee25d9cbcf2119bfc. Full identities are recorded on issue #41.

This was referenced Jul 21, 2026
Open
Merged
Closed
Merged
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Pilot A: protected refutation and derived disproved status

1 participant

@Mnehmos
0