From aefc239c3d265ff6b4548257c07ce30d441e92e4 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 16:20:20 +0000 Subject: [PATCH 1/2] AGENTS.md: Main may mention downstream results but must not depend on them (draft for owner approval) Code Review Rules, "Whole-framework scope", second bullet: the sentence that forbade Main to reference or cite downstream results now forbids dependence on them. It states the permitted mentions (forward pointers, descriptions labelled conditional or proposed, further applications), requires a mentioned result to be identifiable as downstream with its own status, lists what remains barred, and gives the removal test. "Including through indirect labels or unnamed references" now qualifies dependence. The rest of the bullet and the "wholly upstream" bullet are unchanged. No other file restates the old wording, and no tool or guard pins this bullet (R7-MSP pins only the A.35 strings). The rule does not change until the owner approves. Release gate: 21 steps pass; lean-axioms needs the Lean toolchain, which is absent locally (CI covers it). Co-Authored-By: Claude Fable 5.2 Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb --- AGENTS.md | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/AGENTS.md b/AGENTS.md index 496eb7018..5ef8c3a86 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -51,8 +51,18 @@ confers no protection, and "the framework needs this to be true" is never an arg established audits that whole corpus, not Main alone. - `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 + may mention downstream results but must not depend on them, including + through indirect labels or unnamed references. Permitted mentions are + forward pointers to later work, descriptions explicitly labelled as + conditional or proposed, and references identifying further applications; + each mentioned result is identifiable as downstream and carries its own + status where it has one. Main must not use a downstream result to prove + its claims, present a downstream conclusion as established by Main, or + require a downstream theorem for its argument to be valid. Test: removing + every downstream reference must leave Main's proofs, assumptions and + conclusions intact; if removal changes what Main establishes, the passage + contains a dependency, not merely a pointer. + 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 From c101f0d4ce5d48c5b307d0d6b0027c15a41a49ba Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 11 Nov 2026 18:28:10 +0000 Subject: [PATCH 2/2] AGENTS.md: "Permitted mentions include" (open list), per owner decision on #1240 Owner decision (amaybaum, 2026-11-11): "Change to \"include\", merge (Recommended)". ChatGPT review 5863415301 noted the closed list; the removal test and the prohibition on dependence are unchanged. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013T6pfKuv5mi3MXtKjH2tZb --- AGENTS.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/AGENTS.md b/AGENTS.md index 5ef8c3a86..8900fe1ff 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -52,7 +52,7 @@ confers no protection, and "the framework needs this to be true" is never an arg - `papers/Main.md` must be independent of downstream companion papers. Main may mention downstream results but must not depend on them, including - through indirect labels or unnamed references. Permitted mentions are + through indirect labels or unnamed references. Permitted mentions include forward pointers to later work, descriptions explicitly labelled as conditional or proposed, and references identifying further applications; each mentioned result is identifiable as downstream and carries its own