Skip to content

AGENTS.md: theorem recovery before concession - #1047

Merged
amaybaum merged 1 commit into
mainfrom
docs/theorem-recovery-before-concession-20261102
Nov 2, 2026
Merged

amaybaum merged 1 commit into
mainfrom
docs/theorem-recovery-before-concession-20261102

Conversation

@amaybaum

@amaybaum amaybaum commented Nov 2, 2026

Copy link
Copy Markdown
Owner

This is a minimum-change policy PR, authorized by the owner on 2026-11-02 as option (a): the coordinating session writes it, and an independent review and CI follow before the owner's merge decision. It touches AGENTS.md only. Merge is not authorized.

Change

In the "Whole-framework scope" proof-preservation bullet, the owner's "Theorem recovery before concession" text replaces the existing proof-repair sentences rather than adding a second rule. The inserted paragraph is the owner's wording verbatim, except that two missing spaces after full stops were restored:

Theorem recovery before concession. If a mathematical claim lacks a complete independent proof, it must not be presented as established. Before approving a substantive narrowing or withdrawal of an unrefuted mathematical claim solely because its proof is missing or incomplete, reviewers must require a documented, proportionate attempt to recover the proof in the paper where the result logically belongs. The attempt must identify the strongest existing result, its hypotheses and dependencies, the proposed derivation or repair, the verification performed, and the precise remaining gap. A short recovery note within the correction unit is sufficient for a minor gap; substantial theorem gaps require their own scoped, independently reviewed recovery work. Failure to recover a proof is not disproof. Preserve established weaker results and classify the unrefuted stronger claim as open. Relocating a valid result and its proof downstream without weakening it is not a concession and does not trigger recovery. A valid counterexample or disproof requires correction or withdrawal of the refuted claim without delay. An unsupported claim must not remain presented as established while recovery proceeds.

Removed (its content is carried by the new text):

If a genuinely foundational statement lacks an independent argument, seek a separately scoped, independently reviewed proof repair; Main must not present it as established until independently supported. A missing proof in Main does not make a corpus result false. Withdraw a claim refuted by a valid counterexample or disproof; track unrefuted, unresolved stronger claims as open, retaining the strongest verified result with its exact conditions.

The surrounding sentences ("Relocating a valid result is not retracting it from OI." and "Conditional claims may rely on explicitly named hypotheses…") are unchanged. Only the affected lines are re-wrapped.

Review requirements (from the owner)

  1. Integration. No duplicate or conflicting requirements with the rest of AGENTS.md. Content of the removed sentences that the new text does not carry should be flagged, for example "with its exact conditions".
  2. Relocation is not concession. Relocation versus concession must be treated correctly.
  3. Proportion. Recovery effort must be proportionate: a short note for minor gaps, its own unit for substantial ones.
  4. Historical compatibility. An independent audit of S1 (Main posit ledger: second-order posit, A5 scope, external results, Substratum hypotheses (#1029 S1, re-cut) #1043) and S2 (Main conditional and physical claims: relocate downstream content, correct unsupported estimates (#1029 S2, re-cut) #1046) against the new rule, without reopening their merged results unless a genuine inconsistency is found.

In-flight work.

  • P1 satisfies the rule through its documented H-BG recovery attempt.
  • S3's two-condition claim is refuted, so it is withdrawn with no recovery prerequisite. The five-condition theorem keeps its independent proof-verification obligations.

Checks

  • The owner's text appears exactly once after whitespace collapse.
  • The R7-MSP guard's two §A.35 pins are still present.
  • artifact_placement_check passes.
  • No non-ASCII characters in the added lines.

One commit on 06df90c9. #1036 and #1037 stay paused, and the five standing holds are unchanged.


Generated by Claude Code

In the "Whole-framework scope" proof-preservation bullet, replace the
sentences on proof repair and on refuted versus unresolved claims with
the owner-approved "Theorem recovery before concession" text. The
inserted paragraph is the owner's wording; two missing spaces after full
stops were restored. Reviewers must require a documented, proportionate
attempt to recover a missing proof, in the paper where the result
logically belongs, before approving a substantive narrowing or withdrawal
of an unrefuted mathematical claim; the attempt records the strongest
existing result, its hypotheses and dependencies, the proposed repair,
the verification and the remaining gap. A short note suffices for a
minor gap; substantial gaps need their own reviewed recovery work.
Failure to recover is not disproof; relocation without weakening is not
a concession; a refuted claim is corrected or withdrawn without delay;
an unsupported claim is not presented as established meanwhile.

Removed sentences, whose content the new text carries: "If a genuinely
foundational statement lacks an independent argument, seek a separately
scoped, independently reviewed proof repair; Main must not present it as
established until independently supported. A missing proof in Main does
not make a corpus result false. Withdraw a claim refuted by a valid
counterexample or disproof; track unrefuted, unresolved stronger claims
as open, retaining the strongest verified result with its exact
conditions." No other file changes.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb

amaybaum commented Nov 2, 2026

Copy link
Copy Markdown
Owner Author

Exact-head review record: af85622b

(A) Wording: READY. (B) Mechanics: pass. The review was independent. The head is af85622b27a46e977f6486de04057fc857a450a8, single parent 06df90c9, which is main.

Fidelity. The diff is +19/−8 in one hunk. After whitespace collapse:

  • the quoted owner paragraph appears exactly once at the head;
  • the quoted removed text appears once at base and not at the head;
  • replacing one with the other in the base reproduces the head exactly.

The owner supplied the text in the coordinating session rather than on GitHub, so the PR body's quote is the record.

1. Integration. Nothing removed is lost in a way that matters:

  • "With its exact conditions" is covered by the conditional-claims sentence ("every condition carried into the conclusion"), the classification bullet and the Claim/evidence boundary.
  • "A missing proof in Main does not make a corpus result false" is covered by "Failure to recover a proof is not disproof" and the next bullet. This also removes an old redundancy.
  • "Separately scoped, independently reviewed" repair now applies only to substantial gaps. This is a deliberate easing, made for proportion.

There is no conflict with §A.22, §A.25, §A.27, §A.30 or §A.31. F1, F8, F9, F10, F12 and F13 do not regress.

2. Relocation versus concession: correct.

  • Relocating a result with its proof, without weakening, is exempt.
  • Moving an unproved claim downstream is not exempt.
  • A weakening relocation triggers recovery for the weakened part.

3. Proportion. The rule can be applied. However, there is no stated criterion for "minor" versus "substantial", and no decider is named (see R5). By implication, reviewers decide and the owner settles disputes.

4. Historical compatibility.

Optional wording points (non-blocking).

  • R1: two near-duplicate pairs: the relocation sentences, and the two "not presented as established" sentences.
  • R2: inline-heading style, and a short wrapped line.
  • R3: "complete independent proof" should be read relative to each paper.
  • R4: friction with the Claim/evidence boundary when a PR narrows its own overstatement.
  • R5: no criterion or decider for proportion.
  • R6: where "classify as open" is recorded.
  • R7: "solely because" leaves room for narrowings with mixed reasons.
  • R8: whether quantitative physical estimates count as "mathematical claims".

Commit message and PR body. Both are accurate, and nothing paraphrased is presented as verbatim. They say the new text carries all the removed content, which is slightly overstated for the two points that are covered elsewhere.

(B) Mechanics.

  • Only AGENTS.md changes; the paragraph sits at l.100–117 inside the proof-preservation bullet.
  • The R7-MSP pins hold, and there is no other live reader.
  • artifact_placement_check passes.
  • git merge-tree is clean, and the result tree equals the head's tree.

CI at af85622b. Run 41492159459 is green: 25 jobs passed, and 1 (A42 exclusion (${{ matrix.part }})) was skipped by its condition.

No merge is authorized. Merging needs separate exact-SHA approval from the owner.


Generated by Claude Code

@amaybaum
amaybaum marked this pull request as ready for review November 2, 2026 17:47
@amaybaum
amaybaum merged commit 1cfc20f into main Nov 2, 2026
26 checks passed
@amaybaum
amaybaum deleted the docs/theorem-recovery-before-concession-20261102 branch November 2, 2026 17:47

amaybaum commented Nov 2, 2026

Copy link
Copy Markdown
Owner Author

Owner exact-SHA approval and verified normal merge — #1047 theorem recovery policy (2026-11-02)

APPROVED AND MERGED PR #1047 at exact reviewed head af85622b27a46e977f6486de04057fc857a450a8.

  • Independent exact-head review: (A) wording READY, (B) mechanics pass, no scientific/gate blockers.
  • PR CI 41492159459: completed success, 25 passed and 1 conditionally skipped at that exact head.
  • Verified head/base/Main alignment prior to merge, no other file change (only AGENTS.md), clean mergeability. Marked draft ready and used normal GitHub merge with exact expected-head protection.
  • GitHub returned merged=true, merge SHA 1cfc20f6bbf17bc4b45457b9fed59a7464096b3e. Re-fetched: main is exactly that SHA, with parents 06df90c963a452d43bb1eef927b8a62c8bbed5e0 and af85622b27a46e977f6486de04057fc857a450a8, and only AGENTS.md changed.
  • Post-merge main CI 41494497387 was queued when checked. This record does not imply that run passed.

This policy requires a documented, proportionate theorem-recovery attempt before narrowing/withdrawing an unrefuted mathematical claim solely for lack of proof; it exempts unweakened relocation and immediate withdrawal of properly refuted statements. It does not imply that unproved claims remain established during recovery.

#1048 S3 Option B remains a separate draft on older base 06df90c9; its PR CI 41494227213 was still in progress when checked, and no #1048 merge is authorized. H1/H2 decisions are recorded on #1029. #1036/#1037 and five holds unchanged.

amaybaum commented Nov 2, 2026

Copy link
Copy Markdown
Owner Author

Post-merge verification: 1cfc20f6

  • Merge commit: 1cfc20f6bbf17bc4b45457b9fed59a7464096b3e, with parents 06df90c9 (previous main) and af85622b (the reviewed head).
  • Tree: 05d0327856a9cf8f0ac00ddeee175b8f2b4f15cb, identical to the reviewed head's tree. Only AGENTS.md differs from the previous main.
  • main CI on 1cfc20f6: verify, push event, run 41494497387, is green. 25 jobs passed and 1 (A42 exclusion (${{ matrix.part }})) was skipped by its condition.

The theorem-recovery-before-concession rule is now in force. Two history-audit items from the review are open for owner decision:

  • H1: a retroactive recovery note for the two unrefuted Main:224 clauses removed in S2.
  • H2: correcting SM:240's refuted centre-free ⇒ linear claim, and its dependents at Explainer:767 and Structure:301, without delay.

Generated by Claude Code

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants