[amaybaum]

Draft for the owner's approval. The rule does not change until this is approved and merged. A merge is not authorized.

Accountable Issue: #1238. There the owner (amaybaum, 2026-11-11) answered "Yes, draft it" to: "Main may mention downstream results (forward pointers, labelled proposals, further applications) but must not depend on them; test: removing every downstream reference must leave Main's proofs, assumptions and conclusions intact."

Head: aefc239c3d265ff6b4548257c07ce30d441e92e4, one commit on main 082c3eaa. Only AGENTS.md changes (+12/−2).

Why

Read literally, the current text forbids Main from referring to a later paper at all. A trace of Main found 37 downstream references: 15 are forward references, 10 are pointers, 6 are inputs stated in Main, and 6 are dependences. The ruling keeps everything the rule says about dependence and relaxes only bare mention.

The change

Code Review Rules → Whole-framework scope, second bullet.

Before

Main must not reference or cite downstream results, including through indirect labels or unnamed references.

After

Main 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.

The rest of that bullet and the whole "wholly upstream" bullet are unchanged: support within Main, foundational inputs stated with their content and assumptions, role decided by logical dependence, relocation without retraction, and theorem recovery.

Wording choices for the owner to confirm

Choice made	Alternative
Prose inside the existing bullet (that section has no nested lists)	An Allowed / Not allowed / Test sub-list
"conclusions" (the owner's statement)	"scientific conclusions" (the relayed text; narrower)
"Permitted mentions are …" (reads as a complete list)	"such as …" (open-ended)
"if removal changes what Main establishes"	"If it changes what Main establishes" (the relayed wording; antecedent less clear)

Checks

• No other text in the repository restates the old wording. One record applies the rule (verification/audits/manuscript/arrow-1-20261105/RECOVERY.md:775); it concerns an input Main would use, so it is consistent with the new text and is left unedited.
• No tool or guard pins this passage. The only guard that reads AGENTS.md text (R7-MSP) pins two §A.35 strings.
• tools/release_gate.py: 21 steps pass; lean-axioms needs the Lean toolchain and is covered by CI.

No adoption line or lessons-register entry is added, matching that section's style.

Review requested: ChatGPT, at this exact head.

---

Generated by Claude Code

[amaybaum]

ChatGPT independent wording check — ACCEPT / RECOMMEND APPROVAL at exact head aefc239c3d265ff6b4548257c07ce30d441e92e4 (#1240). Read-only assessment of the sole AGENTS.md change; CI run 43057407232 SUCCESS. No change was made or merged.

The replacement implements the owner's ruling: Main may mention downstream work as an identifiable forward pointer, conditional/proposed development, or later application, but its theorem claims, hypotheses and conclusions must remain logically independent of downstream results. The removal test is explicit and useful: stripping downstream references cannot alter what Main proves or assumes. The retained following bullet continues to require independently supported claims and differentiates foundational inputs by actual logical role; the 'wholly upstream' rule still blocks indirect or disguised downstream proof dependencies. Thus the relaxation is editorial, not a weakening of evidentiary requirements.

Minor style note only: “Permitted mentions include” would allow a non-exhaustive catalogue more clearly than “Permitted mentions are”; the current wording's closed list is workable and does not prevent its approval. Recommend owner approve #1240 as written, then handle merging in a separate owner decision. This review does not authorize changes to other files or a merge.

[amaybaum]

Merged as 6122526218411e744588cce3a3fbb13275c7b6b1, a merge commit.

• Owner approval (amaybaum, 2026-11-11): "Change to "include", merge (Recommended)".
• Parents: 1257617a (main), then c101f0d4 (PR head).
• Tree: 0d8701b6. It differs from the PR head's tree only by the changes already on main. Against 1257617a, only AGENTS.md changes (+12/−2).
• CI on the exact head c101f0d4: run 43078077833 green (26 success, 1 matrix placeholder skipped).
• Check: AGENTS.md on main now reads "Permitted mentions include".

Accountable Issue: #1238.

---

Generated by Claude Code