[amaybaum]

This PR adopts the Main proof-independence policy approved by the owner on 2026-11-02 (#1029). It is a separate minimum-change PR, kept apart from the MI-1 corrections. Merge is not authorized.

Change

The PR adds one bullet to AGENTS.md, under "Code Review Rules → Whole-framework scope", directly after the bullet on the whole proof corpus. The text is the owner-approved wording, verbatim and re-wrapped to the section's line width:

papers/Main.md must be independent of downstream companion papers. Main must not reference or cite downstream results, including through indirect labels or unnamed references. Every claim, proof, hypothesis and scope qualification in Main must retain sufficient support within Main, through its own argument or an appropriately cited, independently verifiable theorem or evidence record, with all necessary assumptions explicit. Genuine foundational inputs may be cited as inputs, with their content and assumptions stated. Whether an item is foundational or downstream is determined by its actual logical role, not merely by the paper containing it. Removing a reference without preserving the claim's support is not a correction: unsupported claims must be independently established, narrowed or withdrawn.

The PR changes one file, adding 13 lines and deleting none, in one commit on b26c2ff0.

Scope

• Requirement, not compliance. The bullet states a requirement. It does not assert that Main already complies; that is MI-1's audit and correction sequence on Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029.
• Whole-corpus rule unchanged. The neighbouring bullets ("not the complete proof corpus"; "a proof's absence from Main is not evidence that the result is unproved") are unchanged. A result missing from Main may still be established elsewhere in OI, while Main must independently support any claim it makes.
• Nothing else touched. No manuscript, Lean, ledger, census or generated file changes.

Checks at the head

• The only live check that reads AGENTS.md is the R7-MSP guard (verification/lean/edge_rigidity_probe.py, about :2914). It pins the §A.35 heading and "updates the registry in the same commit"; both are still present after whitespace collapse.
• artifact_placement_check passes, with no unaccounted root artifact.
• legacy_records_check: the self-test passes, but the commit check is undecidable in a shallow local clone. CI runs it with full history. AGENTS.md is not a legacy record.

#1036 and #1037 stay paused, and the five standing holds (#1009, #1023, #1011, #1003, #918) are unchanged.

---

Generated by Claude Code

[amaybaum]

Closed without merging; replaced by #1041.

The exact-head review found the AGENTS.md change correct: the bullet equals the owner's text exactly, and it has no conflicts. The review did find one blocking defect, in the commit message (ef58c7fd): it introduced a paraphrase of the owner's wording as "verbatim". Fixing that would mean rewriting a commit, so the same tree (31520449…) was re-committed instead on docs/main-proof-independence-r2-20261102 as cde5ae2a, with the owner's text quoted exactly.

This branch and commit are kept as provenance.

---

Generated by Claude Code