[amaybaum]

Purpose

Make papers/Main.md strictly upstream and logically independent of all downstream scientific claims and proofs, while locating every canonical proof in the paper whose claims actually need it.

Logical independence: “downstream” is defined by direct or transitive proof dependencies, not where a statement first appeared. Reproducing a downstream argument does not itself prove independence; the premises and complete proof chain (including Lean imports) must be verified independently from Main's foundations and genuine external inputs.

F13 correction — define Main's proof roots:

• The starting points are Main's declared foundational contributions: its headline theorems and characterizations, and the statements of their premises and scope. These are retained even when no further Main result consumes them.
• Auxiliary results are retained and proved in Main only if one of those foundational roots depends on them, directly or transitively. Merely stating a result in Main does not make it a foundational root.
• When a result has no Main consumer, place it, with its necessary proof, in the upstream-most downstream paper that needs it. Relocation is not scientific retraction.
• When Main proves a result, downstream papers cite Main instead of duplicating its proof. This does not prohibit required book/FULL/Explainer mirrors, independent Lean checks, or genuine downstream extensions.
• Named hypotheses may remain justified, posited or open, provided conditional conclusions retain their assumptions. Refuted claims are withdrawn; unrefuted stronger claims with incomplete proofs remain open.

Review history and scope

• c5bd41bc: NOT-READY F1 — refuted vs unresolved.
• 61c97030: NOT-READY F8 — open/posited conditional hypotheses.
• 84a84124: READY-WITH-NITS and green CI, F1 and F8 resolved at that head.
• cb4047c9: NOT-READY F12 — first-publication/proof-dependency ambiguity.
• 1fc7299c: independent READY wording, successful mechanics and CI, F12 resolved.
• ae92137d8d006003add27ed4f08f70ca0533c900: independent REVISE F13; reviewer found the ambiguous test “no Main claim depends on” could wrongly remove Main's own headline theorems, or else fail to remove auxiliary results. Exact-head review record. Mechanical checks passed at that head, but do not transfer.
• Current fad8a269ca5c5159988d28eb3b9775a49e40bba9: author corrected only the new rule bullet to define foundational roots and supporting auxiliary results, and to preserve proof relocation, mirrored-book exceptions, Lean verification and downstream extensions. Independent exact-head review and fresh CI are pending.

Changes: AGENTS.md only, one new rule bullet; no scientific manuscript, formal proof, grade, LEDGER, verification code or generated artifact changes.

Gates: This draft does not certify Main's present compliance. S1 was merged via #1043. S2 is authorized for implementation as a separate draft PR with O1–O7 decisions; O6 is new text requiring full independent exact-head review, and O3/O4 plus stale downstream references remain deferred. Further S3/P1/C1/C2/L1 stages and the downstream proof de-duplication unit remain separately gated. #1036, #1037 and the five standing holds remain unchanged.

Do not merge this PR until fresh independent exact-head review, green CI, clean mergeability and a separate exact-SHA owner approval.

[amaybaum]

Owner-forwarded independent review of c5bd41bc — NOT-READY (F1 blocking)

Provenance: owner supplied the separate reviewer’s verdict in chat. This is an owner-posted report of that review, not a claim that a reviewer authored this GitHub comment. Exact assessed PR head: c5bd41bc5c251ee1fbf0a3b5d6605596583fe3dd.

Verdict: NOT-READY. The reviewer verified the AGENTS-only diff, unchanged existing guard strings, clean merge and the ordinary CI 41464813687 (25 succeeded, one expected skip). The policy still has a scientifically significant logical conflation:

F1 (BLOCKING): “A refuted inference or an unresolved proof gap ... track the stronger claim as an open proof obligation or conjecture” misclassifies a refuted claim as open. A concrete counterexample refutes the claim as stated; an unresolved proof gap does not. The existing §A.30 and merged proof-independence rule require withdrawal of refuted/unsupported overclaims, not preservation under a new label.

Required minimum correction: “A claim refuted by a counterexample is withdrawn. A broken inference or an unresolved proof gap must not be presented as established: retain the strongest verified result with its conditions, and track the stronger claim, unless refuted, as an open proof obligation or conjecture.”

PR description: resolve its analogous conflation as part of the same review correction.

Optional improvements (not blockers): interim Main wording while a repair is open; replace unbounded “bounded” or connect it to an existing stop rule; include adequate evidence records at their proper status and independence of the imported proof from downstream papers; distinguish an invented rescue premise from a legitimate conditional result with a stated hypothesis.

Disposition: F1 accepted. The PR is held; do not merge the reviewed head. The author will make a single narrowly scoped correction on the draft branch, request fresh exact-head scientific/editorial review and CI, and return for separate exact-SHA merge approval. No manuscript edits or holds changed.

[amaybaum]

F1 revision checkpoint — new exact head 61c97030 (NOT YET REVIEWED)

The initial independent NOT-READY verdict on c5bd41bc was preserved in comment 6580420252. F1 has now been corrected in the AGENTS.md bullet and PR body, by one append-only branch commit 61c9703073b4f6553804dcc96aa9da08d880d782.

• Refuted: “A claim refuted by a counterexample is withdrawn.”
• Unresolved: Retain the strongest verified conditional result and track only the unrefuted stronger claim as an open obligation/conjecture.
• Proof preservation: add sufficient standalone proof, exact kernel citation or appropriately graded evidence record, with complete hypotheses and no downstream proof dependency.
• Interim scope: while repair is open, Main states only what is verified; the repair is separately scoped and independently reviewed.
• Premises: an independently justified named conditional hypothesis is legitimate; unsupported ad hoc rescue premises are forbidden.
• No other file changed. PR remains draft, unmerged; current diff against main is AGENTS.md only, 18 additions, zero deletions; main has advanced through S1 Main posit ledger: second-order posit, A5 scope, external results, Substratum hypotheses (#1029 S1, re-cut) #1043 to b87733a4, with no AGENTS content conflict.
• New automatic PR CI 41467689609 was queued at last inspection. This does not inherit the old green result: require a fresh exact-head independent scientific/editorial review, green CI and separate explicit exact-SHA merge approval.

The five holds and paused #1036/#1037 are unchanged. No manuscript, scientific result, theorem grade or policy merge occurred in this revision.

[amaybaum]

Exact-head review record: c5bd41bc (superseded head)

Verdict: NOT-READY. One substantive finding (F1); the rest passed. The review was independent. The head was c5bd41bc5c251ee1fbf0a3b5d6605596583fe3dd on main a65fe8a8. This record is kept as the owner directed; the owner has since corrected the PR at 61c97030, which is reviewed separately.

Mechanical checks (all passed).

• Only AGENTS.md changes, with 14 lines added and none removed. The new text sits directly after the Main proof-independence bullet, and removing it restores the base byte for byte.
• The R7-MSP guard's two pinned §A.35 strings are still present, and no other live check reads or hashes AGENTS.md.
• artifact_placement_check passes.
• git merge-tree is clean, and its result tree equals the head's tree.
• CI run 41464813687: 25 jobs passed and 1 was skipped.

F1 (substantive, blocking). The sentence "A refuted inference or an unresolved proof gap must not be presented as established: retain the strongest verified result with its conditions, and track the stronger claim as an open proof obligation or conjecture, including any counterexamples" applies both outcomes to both cases. A claim refuted by a counterexample is false, not open.

As written, the sentence conflicts with:

• the owner's stated intent;
• the merged bullet's "withdrawn" outcome;
• §A.30, under which a claim that loses its support is removed, not tagged.

It would also require S1's refuted gauge-invariance ⇔ linearity equivalence to be tracked as an open conjecture.

Minimal fix: a claim refuted by a counterexample is withdrawn, and only an unrefuted stronger claim is tracked as open. The owner accepted this.

Optional wording points (non-blocking).

• F2: What Main asserts while a repair is under way.
• F3: "Bounded" has no stated limit and no one named to decide it.
• F4: Accepted support should also include a theorem or evidence record, and the imported proof should have no downstream dependency.
• F5: Distinguish a rescue premise from a result stated as conditional on a named hypothesis.
• F6: Repeat "within Main" in the fallback.
• F7: "A missing proof in Main is not a disproof" duplicates the next bullet.

In-flight work. S1 (#1043) needs no change once F1 is fixed. P1's plan is consistent with the rule, which adds these obligations:

• every hypothesis of an imported proof is stated in Main;
• the imported proof has no downstream dependency;
• on fallback, the stronger claim is tracked as open unless refuted;
• hclass is stated as a named condition.

---

Generated by Claude Code

[amaybaum]

Exact-head review record: 61c97030

Verdict: NOT-READY. F1 is resolved, but one new substantive finding (F8) blocks. The review was independent. The head is 61c9703073b4f6553804dcc96aa9da08d880d782 (parent c5bd41bc), and main is now b87733a4, the #1043 merge, which did not touch AGENTS.md.

Mechanical checks (all passed).

• Only AGENTS.md changes, with all edits inside the one bullet: +18/−0 against a65fe8a8, +14/−10 against c5bd41bc.
• The bullet sits directly after the proof-independence bullet, and removing it restores the base byte for byte.
• Both R7-MSP strings are still pinned. The only live reader of AGENTS.md is unchanged.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean. The merged AGENTS.md equals the head's, and no other path differs from b87733a4.
• CI: pull-request run 41467689609 was still in progress at review time, with 20 jobs passed, 1 skipped and 4 running.

F1: resolved. "A claim refuted by a counterexample is withdrawn" stands alone. "Unless refuted" prevents tracking a refuted claim as open. The retention clause still keeps the valid weaker part of a refuted claim, as S1 kept the affine restriction.

F8 (substantive, blocking). "Legitimate conditional results may name independently justified hypotheses" naturally reads as allowing a conditional result only when its hypotheses are justified. That conflicts with:

• the audit method's C class, "conditional on a stated open assumption", and the open named hypotheses (e.g. H-χ, H-spin);
• the review rule to classify claims "by whether it is conditional on named hypotheses";
• the Claim/evidence boundary's narrowing path;
• this bullet's own "retain … with its conditions";
• the planned P1 fallback to hclass, a hypothesis that could not be justified;
• S1's merged posits A5 and (xiii), which are explicitly not derived.

Minimal fix: make legitimacy depend on the hypothesis being explicit and status-labelled, with the conclusion stated as conditional. Keep the ban on premises that are unstated or ad hoc, or used to present a conditional result as established.

F2–F7.

• F2 and F4 are addressed.
• F3 is replaced by "separately scoped". It has no stopping rule, but the fix for F2 makes that harmless.
• F5 is addressed in intent, but its new sentence is where F8 comes from.
• F6 is partly addressed.
• F7 is unchanged, which is acceptable.

Optional wording points (non-blocking).

• F9: "Main states only what is already verified" does not say where the verification is.
• F10: "refuted by a counterexample" is narrower than refutation by a disproof.
• F11: the articles in the support-forms list are inconsistent.

PR body and comments.

• The body calls F3 "unbounded" rather than "bounded", and repeats the F8 wording.
• Comment 6580420252 quotes "Required minimum correction" text as if from the earlier review, which supplied no such wording.

In-flight work.

• S1 is consistent once F8 is fixed: it withdraws the refuted equivalence and keeps the affine result.
• P1:
  • its order matches the rule;
  • Main must state only what is verified while the repair is under review;
  • the BG-2-refuted premise is withdrawn;
  • if S1's counterexample also refutes the SM:240 and Explainer:767 assertions, they are withdrawn rather than made conditional. This has not been checked.

No merge is authorized.

---

Generated by Claude Code

[amaybaum]

F8 revision and review-provenance correction — head 84a84124 (2026-11-02)

The reviewer’s second NOT-READY verdict for exact head 61c97030 is preserved verbatim in comment 6580629776. F1 remained resolved; F8 was blocking.

New current commit: 84a841248a677d3273b598ab67c66964ad5a8995, append-only child of 61c97030. The only changed source is the new AGENTS.md proof-preservation bullet; no Main/SM/manuscript/Lean/ledger/CI config was edited. The PR body was updated too. Against main b87733a4, the diff is only AGENTS.md (22 added lines, no deletions), and the PR remains a cleanly mergeable draft.

F8 correction: a conditional result may assume a named, explicitly stated, status-labelled hypothesis, whether independently justified, a selected posit, or genuinely open; carry that condition into its conclusion. An open/posited hypothesis is not misrepresented as physically sourced. No ad hoc or unstated premise may be used to assert an unconditional result. The source now also distinguishes disproof from a counterexample and clarifies what Main can present as established while a proof repair is pending.

Provenance correction: the “Required minimum correction” wording in my earlier owner-posted comment 6580420252 was my paraphrase/proposed replacement, not a literal quotation from the independent reviewer. The independently supplied review record at 6580515904 is authoritative for that review. No historical comment is silently rewritten.

Current gate: automatic fresh PR CI 41469860868 is in progress, and the latest head has not been independently reviewed yet. Do not infer readiness from the old green CI. Require an independent exact-head scientific/editorial review, completed green CI and separate owner exact-SHA merge approval; this comment does not authorize merge.

Separate operations: S1 #1043 merged at b87733a4; superseded S1 #1042 is now closed unmerged; S2 has been authorized for proposal and review only on #1029. #1036 and #1037 plus the five holds remain unchanged.

[amaybaum]

Exact-head review record: 84a84124

Verdict: READY-WITH-NITS. The review was independent. The head is 84a841248a677d3273b598ab67c66964ad5a8995, with chain 61c97030 → c5bd41bc → a65fe8a8. main is b87733a4.

Findings resolved.

• F8: resolved. A conditional result may rest on a hypothesis that is named, stated, labelled justified, posited or open, and carried into the conclusion. This covers:

  • the audit's C and L classes, and open named hypotheses such as H-χ, H-spin and (EM);
  • classification by named hypotheses;
  • S1's A5 and posit (xiii);
  • P1's hclass fallback.

  Unstated or ad hoc premises, and presenting a conditional result as unconditional or derived, stay barred.

• F1: not regressed. A claim refuted by a valid counterexample or disproof is withdrawn, and only an unrefuted stronger claim is tracked as open.

• F10: addressed (disproof now included).

• F9: resolved. The interim clause limits only what Main presents as established.

No substantive conflict was found with the rest of AGENTS.md.

Mechanical checks.

• Only AGENTS.md changes: +22/−0 against a65fe8a8, inside one bullet placed directly after the proof-independence bullet. Removing it restores the base byte for byte.
• Both R7-MSP strings are still pinned, and the only live reader of AGENTS.md is unchanged.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean. The merged AGENTS.md equals the head's (edff0403), and every other path equals b87733a4.

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

Optional wording points (non-blocking).

• N1: "merely to rescue" could be read as qualifying the ban on presenting a conditional result as unconditional. The Claim/evidence boundary bans that anyway, so this opens no loophole.
• N2: "ad hoc" is undefined. A cross-reference to §A.29's hard-to-vary test would settle it.
• N3: "(justified, posited or open)" could read as exhaustive. Empirical inputs fit under justified or posited.
• F11: a cosmetic article inconsistency remains.
• N4: the PR body's "do not disguise an ad hoc premise" is weaker than the text, which bars introducing one.
• N5: comment 6580773815 calls comment 6580629776 a "verbatim" copy of the second review. That comment is a condensed record, and its F8 summary adds a "physically sourced" clause that the rule text does not contain. This affects the review history only.

In-flight work.

• S1 needs no change.
• P1's plan is consistent with the rule, which gives it these obligations:
  • imported proofs state every hypothesis and have no downstream proof dependency;
  • during review, Main presents as established only what Main itself supports;
  • on fallback, hclass is labelled open and carried into the conclusion;
  • the premise refuted in BG-2 is withdrawn;
  • SM:240 and Explainer:767 are withdrawn if S1's counterexample refutes them (not yet checked).

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

---

Generated by Claude Code

[amaybaum]

Owner architectural clarification — policy revision at d42695fa (review pending)

The independent READY-WITH-NITS review at 84a84124 and green CI 41469860868 are preserved. They do not apply to the new head d42695fa6af9766dfa23b4eb8650c57452d16c3a, which supersedes the reviewed head without merging.

The owner clarified a key distinction: Main should not contain claims that logically depend on mathematics developed downstream merely because those claims can be saved by copying proofs into Main. The dependency should flow Main → Substratum/SM/GR, never back. For a downstream-dependent Main claim, default to relocating the valid claim and its proof downstream, retaining its correctness in the corpus. Import sufficient mathematical support into Main only when independent review confirms that the result genuinely belongs to Main's foundational scope and the imported argument has no downstream logical dependency. This is a rule about paper architecture, not a demand to abandon proved mathematics.

Change at the new exact head: only the existing draft proof-preservation bullet in AGENTS.md was rewritten at its opening; the previously reviewed F1 (refuted vs unresolved) and F8 (named justified/posited/open hypotheses with condition explicitly carried) distinctions remain. The PR body was revised. No manuscripts, theorem grades, Lean, guards, or CI files changed.

Current status: draft and unmerged; independently review this exact new head, including compatibility with the existing Main-independence rule and every review finding. Require fresh green CI, clean mergeability and separate owner exact-SHA approval. No merge is authorized by this correction. The five holds and #1036/#1037 unchanged.

[amaybaum]

Owner instruction: Main must be entirely independent of downstream science and proofs — revised exact head cb4047c9

In response to the owner's explicit requirement, #1044's proposed policy now states that Main must be completely logically independent of every downstream scientific claim and mathematical proof, not merely uncited. It forbids direct or indirect dependence on downstream claims, proofs, lemmas, calculations, or renamed/hidden imports through Lean. It also forbids copying a downstream proof into Main simply to make the dependency invisible. Main can independently derive a statement also discussed downstream only from genuinely upstream foundational premises and checkable evidence with no downstream proof dependency. Any downstream-dependent Main claim is to be relocated downstream by default, preserving valid OI mathematics there.

Current exact head: cb4047c97352a180504ea9c5415d95501030cb00 (child of d42695fa). The other provisions remain: a valid counterexample/disproof refutes a claim, a missing proof is not disproof, and genuinely conditional claims may name justified, posited or open hypotheses without treating them as derived.

Current status: draft, unmerged. The previous READY-WITH-NITS at 84a84124 and its green CI do not authorize or establish readiness of this head. Re-review this exact commit for scientific architecture, accidental loopholes, retained F1/F8 fixes, and consistency with the preexisting Main-independence rule. Recheck ordinary CI and mergeability. Seek a separate exact-SHA merge decision, not an automatic merge. No manuscript changes or holds affected.

[amaybaum]

Exact-head review record: cb4047c9

Verdict: NOT-READY. One substantive finding (F12). Everything else passes or is optional. The review was independent. The head is cb4047c97352a180504ea9c5415d95501030cb00, with chain d42695fa → 84a84124 → 61c97030 → c5bd41bc → a65fe8a8; d42695fa was not reviewed at its own head. main is b87733a4.

Mechanical checks (all passed).

• Only AGENTS.md changes: +30/−0 against base, in one bullet placed after the proof-independence bullet. Removing it restores the base byte for byte.
• The R7-MSP pins hold, and there is no other live reader of AGENTS.md.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean. The merged AGENTS.md equals the head's blob 217cd133, and no other path differs.
• CI run 41472512582: 25 jobs passed and 1 was skipped.

F12 (substantive, blocking). The owner's stated rule (#1029 comment 6581235865) is: "Main may independently establish a mathematical statement that also appears in a downstream paper. However, neither its premises nor its justification may depend on downstream scientific results or mathematical proofs. Reproducing a downstream proof without establishing that independence does not satisfy this requirement."

The first two sentences are in the text. The third is not. Instead, line 70 reads unconditionally: "Do not cite, rely on, copy, adapt or repackage a downstream claim, proof, lemma or calculation as Main's justification". "Downstream proof" is never defined. That permits a provenance reading: nothing that first appeared downstream may be reproduced, even once its independence is established. Under that reading the line:

• is stronger than the owner's rule;
• conflicts with lines 72–75, which permit independent establishment;
• conflicts with the merged bullet's "actual logical role, not merely by the paper containing it".

The burden of establishing independence is also only implicit.

Smallest fix, in the owner's words: make line 70's ban on copying or adapting conditional on independence not being established, or define "downstream" for proofs, lemmas and Lean theorems by logical dependency.

Optional wording points (non-blocking).

• N6: no stated test for when a Lean theorem is downstream. The owner's Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 criterion, its logical proof dependencies, would close this.
• N7: for a foundational claim whose only proof is downstream, the order of relocation and repair is not stated.
• N8: relocating a claim affects the Main claims that use it. Existing rules cover this.
• N9: "justified" should mean justified without downstream support.
• N10: the absolute "wholly upstream" wording is fine. The remaining Substratum citations are MI-1 obligations, and a transitional note would be work-plan detail.
• N11: the "missing proof" sentence is redundant, "ad hoc" is undefined, and the PR title no longer matches the rule.
• B1: the PR body names specific downstream papers, which the rule text does not.
• B2: the PR body's "moving its proof into Main does not remove the logical dependency" states the broad reading.

No regressions. F1, F8, F9, F10 and N1 stay resolved.

S1's item (vii) argument complies. The telescoping step uses only the stated hypothesis and the abelian group that posit (xiii) supplies. A5 is posited. Its appearance in SM and Substratum creates no dependency.

P1 consequences. P1 needs an independence audit of the H-BG argument, including the transitive Lean dependencies of the hclass theorems in CongruentReconstruction and RootedClassification. If independence fails, the claim is relocated to GR. The text also still permits a conditional lemma on an open hclass or H-BG hypothesis, stated in Main's terms. Excluding that route for P1 is a plan decision.

Commit messages and #1029 comment 6581125941. Both commit messages are accurate. The comment is accurate and labelled; it carries the same copy/adapt ambiguity, and its Lean criterion is clearer than the AGENTS.md text.

No merge is authorized.

---

Generated by Claude Code

[amaybaum]

F12 correction — current exact head 1fc7299cea20f6d5aa6ce5226d6446634d5aa443 (independent review pending)

The independently posted NOT-READY review of cb4047c9 found F12: the unconditional “copy/adapt” prohibition could classify a proof as downstream by publication provenance rather than logical dependency, inconsistent with the owner’s actual rule.

Owner-intended interpretation explicitly implemented: a mathematical result or Lean theorem is downstream for Main precisely when its direct or transitive logical proof dependencies require downstream-specific scientific claims, premises or mathematical results — not simply because the argument was first written in a companion paper. Main may independently prove a statement that also occurs downstream, but must demonstrate independence of all premises and proof steps. Merely copying, rephrasing or moving an existing proof does not by itself prove independence. The policy continues to require relocation of truly downstream-dependent claims, preservation of proved mathematics in its appropriate home, withdrawal of refuted claims and honest conditional hypotheses.

Author revised only the new AGENTS.md bullet, plus the PR body; no manuscripts, proof grade or verification files changed. The earlier review and old green CI do not carry over to this head. Require fresh independent exact-head review, ordinary CI and separate owner SHA-specific merge decision. This is draft/unmerged.

The in-flight MI-1 S2 proposal/review under #1029 remains proposal-only; no manuscript commit or scientific execution authorized by this correction. #1036/#1037 and the five holds remain unchanged.

[amaybaum]

Exact-head review record: 1fc7299c

(A) Logical-independence wording: READY. (B) Mechanical checks: pass. The review was independent. The head is 1fc7299cea20f6d5aa6ce5226d6446634d5aa443 (parent cb4047c9), and main is b87733a4.

(A) Wording. F12 is resolved. Each part of the owner's distinction is in the text:

• First appearance does not disqualify: l.72–73, "not merely because it first appeared in another paper".
• Dependence disqualifies: l.69–72. An item is downstream when "its direct or transitive logical dependencies require downstream-specific science or mathematics". Line 73 adds "Main must not rely on such support", and l.67–69 extend this to premises.
• Reproduction alone proves nothing: l.75–77, "Reproducing an argument from a downstream paper does not by itself establish independence: its premises and all proof dependencies must be checked…". This is stated as an obligation.

No provenance reading remains. "Copy, adapt or repackage" is gone. "Relabelled/hidden" and "do not transplant" now apply to support defined by dependency. N6 is resolved: Lean theorems fall under the transitive-dependency test. There is no new substantive conflict with AGENTS.md, and F1, F8, F9 and F10 stay resolved.

Optional wording points (non-blocking).

• N12: "downstream-specific" leaves the base case to the logical-role test.
• N13: "require" could be read modally. l.75–80 close that reading.
• N9 (extended): a named hypothesis labelled posited or open must also lie within Main's scope. This is implied, not stated beside the conditional clause.
• N7, N8, N10, N11: unchanged. N11 includes the stale PR title.
• PR body:
  • B1: it still lists Substratum among the "downstream" papers.
  • B3: "can be independently derived" is weaker than the text's "be independently established".
• Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 comment 6581421373 (B4): "cannot be independently established → relocate" leaves out the rule's repair route for genuinely foundational statements and its conditional-hypothesis route.

(B) Mechanics.

• Only AGENTS.md changes: +35/−0 against base, in one bullet (l.66–100) placed after the proof-independence bullet. Removing it restores the base byte for byte. The text is ASCII-only, with no line over 76 columns.
• Both R7-MSP strings are still pinned, and the only live reader of AGENTS.md is unchanged.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean. The merged AGENTS.md equals the head's blob 5cd11358, and only AGENTS.md differs from main.
• The commit message and comment 6581418153 are accurate.

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

In-flight work.

• S1: the item (vii) argument still complies.
• P1: needs an independence audit of the H-BG argument, including its transitive Lean dependencies. If that fails, the claim is relocated to GR. A lemma conditional on a labelled-open hypothesis, stated in Main's own terms, remains permitted.

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

---

Generated by Claude Code

[amaybaum]

Owner decision (a): add proof-placement / no-duplication rule in this PR — new exact head ae92137d8d006003add27ed4f08f70ca0533c900

The owner explicitly chose (a) over merging 1fc7299c and later adding a new PR. Two sentences were added inside the existing new AGENTS.md bullet, using only line-wrap changes:

Main does not prove a result merely because a downstream paper uses it or to replace a downstream citation: a result that no Main claim depends on belongs in the downstream paper and is removed from Main. When a result is proved in Main, downstream papers cite Main's proof instead of repeating it.

This addition is consistent with the separate rule that Main may independently establish an actually needed mathematical statement even when the same statement also appears downstream, provided its premise and transitive proof dependencies are upstream. Main-necessity now governs proof placement: if no Main claim needs a result, leave that result downstream, without withdrawing valid mathematics from OI. The canonical mathematical proof belongs to the upstream-most paper that needs it; other papers cite it. Formal verification can remain linked as evidence without justifying duplicated narrative proofs.

Earlier review is not transferrable. The independent review of 1fc7299c found its wording READY and mechanics passed, but it does not review this newly changed head. Request fresh independent exact-head wording/consistency review, CI at this SHA and mergeability confirmation. Specifically inspect the two sentences for whether every Main result needs a dependent Main claim, whether “downstream papers cite Main” permits necessary independent Lean checks or concise application summaries, and whether the rule keeps physical/scientific proof dependencies upstream. No automatic merge.

PR remains draft/unmerged. Only AGENTS.md is modified. S2 proposal review and #1029's other units remain separately gated; the future downstream de-duplication audit is not included in S2. Holds unchanged.

[amaybaum]

Exact-head review record: ae92137d

(A) Wording: REVISE (F13). (B) Mechanics: pass. The review was independent. The head is ae92137d8d006003add27ed4f08f70ca0533c900 (parent 1fc7299c), and main is b87733a4.

What changed since 1fc7299c: +6/−2 in one hunk, inserting l.80–84: "Main does not prove a result merely because a downstream paper uses it or to replace a downstream citation: a result that no Main claim depends on belongs in the downstream paper and is removed from Main. When a result is proved in Main, downstream papers cite Main's proof instead of repeating it."

F13 (substantive). The removal test "a result that no Main claim depends on … is removed from Main" never says which results count as the starting points. It allows two readings, and neither matches the owner's intent:

• Literal reading. Only results that another Main result consumes are kept. Main's headline theorems, such as the QM equivalence, the characterization theorem and the continuum realization theorem, are the ends of their chains. Nothing consumes them, so the rule could send them downstream.
• Generous reading. Every result stated in Main counts as needed. That protects S08-type claims that Main states only for downstream use, so the rule would remove nothing.

The first clause ("not … merely because a downstream paper uses it") has the right criterion, but the sentence after the colon is the one reviewers will apply.

Smallest fix, in the owner's words: name the starting points. Main's own results within its foundational scope (its stated theorems, its contribution and the scope statements about its premises) are needed in their own right. Any other result stays only if one of these depends on it, directly or transitively.

Optional wording points (non-blocking).

• N14. The text does not say that the proof moves with a relocated result. Without that, removing a proof that downstream papers cite would leave them citing nothing. It also does not say where the result goes when several papers use it; the owner's Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 comment says the upstream-most one.

• N15. "Cite Main's proof instead of repeating it" should not cover:

  • the book, FULL and Explainer, which mirror Main under §A.14 and §A.25 step 3;
  • Lean verification or downstream extensions, which the Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 comment exempts but the text does not.

  Restating a result downstream stays allowed; only repeating the proof is barred.

• N16. The present tense states a rule, not a claim that the corpus already complies. Keeping the de-duplication audit on Correction planning: cross-references, labels, ledger/census and evidence records (from the 2026-11-01 disposition) #1029 rather than in AGENTS.md is right.

Other checks. No collision with Whole-framework scope bullet 1. No regression of F1, F8, F9, F10 or F12.

(B) Mechanics.

• Only AGENTS.md changes: +39/−0 against base, in one bullet (l.66–104). Removing it restores the base byte for byte.
• Both R7-MSP pins hold, and there is no other live reader of AGENTS.md.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean, and only AGENTS.md differs.
• CI run 41476585658 was still running at review time; the previous head's run was green.

Accuracy. The commit message, PR title and PR body are accurate. Comment 6581698798 repeats the F13 test and adds the upstream-most placement and the exemptions, neither of which is in the text yet.

No merge is authorized.

---

Generated by Claude Code

[amaybaum]

F13 resolved in draft text — new exact head fad8a269ca5c5159988d28eb3b9775a49e40bba9 (fresh review pending)

The independent REVISE verdict at ae92137d identified F13: the former “no Main claim depends on” rule had no explicit roots and could remove Main's own headline theorems or treat every stated result as its own justification.

Proposed fix now implemented in AGENTS.md, with no other file edited:

• Main's declared foundational contributions—headline theorems, characterizations and the statements of their premises and scope—are the starting roots of its proof/dependency graph. They remain Main's contributions even without a later Main theorem consuming them.
• An auxiliary result belongs in Main only when one of those roots depends on it directly or transitively. Simply asserting a result in Main does not convert it into a root. A result needed only downstream is moved with necessary proof support to the upstream-most downstream paper needing it.
• When Main proves a result, downstream papers cite the Main proof instead of duplicating it; this does not bar required book/FULL/Explainer mirrors, independent Lean verification or genuinely new downstream extensions.
• Prior safeguards remain: downstream defined by logical (including transitive) dependency rather than publication provenance; independent proof must be audited; no downstream-specific premise in Main, no false unconditional claim, posited/open named hypotheses may support clearly conditional results, refuted claims are withdrawn.

The exact changed head is fad8a269ca5c5159988d28eb3b9775a49e40bba9. Earlier review/CI at ae92137d cannot certify this new head. Request independent scientific/editorial exact-head review, paying special attention to F13's roots definition, the mirror/Lean/extension exceptions, absence of downstream imports, and regressions of F1/F8/F9/F10/F12. Require fresh ordinary CI and mergeability, then separate owner exact-SHA merge approval. The PR remains draft and unmerged.

Separately, S2 O1–O7 were approved for a draft PR from b87733a4. Its newly drafted O6 (Main:224) text must be reviewed in full after implementation; approvals of S2b do not pre-accept O6. No book edits are authorized. #1036/#1037 and all five holds remain unchanged.

[amaybaum]

Exact-head review record: fad8a269

(A) Wording: READY. (B) Mechanics: pass. The review was independent. The head is fad8a269ca5c5159988d28eb3b9775a49e40bba9 (parent ae92137d), and main is b87733a4.

(A) Wording. git diff ae92137d fad8a269 is +13/−5 in one hunk, replacing l.80–84 with l.80–92.

F13 is resolved. Main's "declared foundational contributions … headline theorems and characterizations, and the statements of their premises and scope" are the roots of its proof graph:

• Roots "need not be consumed by another Main result", so the literal reading can no longer send headline results downstream.
• "Merely stating a result in Main does not make it a root", so the generous reading can no longer keep everything.
• Auxiliary results stay in Main only if a root depends on them, directly or transitively.

Test cases.

• QM equivalence and characterization: roots; they stay.
• Posit (xiii): a premise statement, so a root.
• S08 condensate clause: not a root, so it is relocated unless a root depends on it.
• S1 item (vii): needed through the A5 scope statement.
• U10: stays if a premise or scope statement in Main asserts or relies on the independence of A4's clauses; otherwise it is auxiliary.
• Continuum realization theorem: depends on whether it is declared a headline result (see N17 below).

N14 and N15 are resolved. Relocated results move "together with their necessary proofs to the upstream-most downstream paper that uses them". The exemption covers only "required" book/FULL/Explainer mirrors, independent Lean verification and "genuinely new" downstream extensions, which does not license re-proving Main results.

No regressions. F1, F8, F9, F10 and F12 stay resolved. No new conflict with AGENTS.md.

Optional wording points (non-blocking).

• N17: "declared" does not say where the declaration lives, so middle-rank theorems need a judgement.
• N18: extensions are not told to cite Main for the part Main proves; an unneeded result that no downstream paper uses has no destination; and "upstream-most" is undefined between sibling papers.
• N19: "to replace a downstream citation" could be misread as blocking the repair route for a result a root needs. "Merely" and the root test already permit it.
• Carried over: N7–N10, N12 and N13; and from N11, the redundant "missing proof" sentence and the undefined "ad hoc". The PR body's "no Main consumer" reuses older wording.

(B) Mechanics.

• Only AGENTS.md changes: +47/−0 against base, in one bullet (l.66–112). Removing it restores the base byte for byte. The text is ASCII-only with lines of at most 76 columns.
• Both R7-MSP pins hold, and there is no other live reader of AGENTS.md.
• artifact_placement_check passes.
• git merge-tree against b87733a4 is clean. The merged AGENTS.md equals the head's blob (fe79d6b0), and only AGENTS.md differs.
• The commit message and comment 6581928298 are accurate.

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

In-flight work.

• S1 complies.
• P1: H-BG stays in Main only if a root depends on the phase-locking lemma. That is plausible through the QM equivalence chain but not checked, and it is subject to the independence audit if kept; otherwise it stays in GR.
• S2: the S08 and U10 sites now have a definite test.

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

---

Generated by Claude Code

[amaybaum]

Owner exact-SHA merge approval and verified normal merge — 2026-11-02

APPROVED AND MERGED #1044 at exact reviewed head fad8a269ca5c5159988d28eb3b9775a49e40bba9.

• Independent exact-head review: (A) READY wording, F13/N14/N15 resolved, earlier blockers F1/F8/F9/F10/F12 not regressed; (B) mechanical gates pass.
• Exact-head CI 41478306862: completed/success, 25 jobs passed, 1 skipped by condition.
• Verified the PR still had this exact head, changed only AGENTS.md (+47/−0) and merged cleanly onto main b87733a400c563592774dad2a61425c7663b69d1.
• Changed draft to ready, used GitHub normal merge with expected_head_sha enforced; GitHub returned merged=true and merge commit 1482b90eb5b6de2f08296daf4606b7ecfe9cdfa7.
• Independently re-read main: main = 1482b90eb5b6de2f08296daf4606b7ecfe9cdfa7, merge parents precisely b87733a4 and fad8a269, with AGENTS.md as the only changed file.
• Post-merge main CI 41480334252 is queued, not yet green. Do not describe that run as passed.

Scope: This merge adopts the upstream-only Main policy and the proof-root/auxiliary placement and de-duplication principles. It does not certify present papers/Main.md as compliant, supply or promote any mathematical theorem, or authorize further manuscript edits. S2 #1045 still has independent review and CI running and requires a separate exact-SHA decision. U10 remains in Main only if the S2 review establishes its role as a stated foundational-premise/scope root or a needed supporting result; otherwise return it for disposition. #1036/#1037 and the five holds remain unchanged.

[amaybaum]

Post-merge verification: 1482b90e

• Merge commit: 1482b90eb5b6de2f08296daf4606b7ecfe9cdfa7, with parents b87733a4 (previous main) and fad8a269 (the reviewed head).
• Tree: bd826a24d074237f82fcdce3a50ccb96f01335f4. This is identical to the reviewed git merge-tree result of b87733a4 and fad8a269. It differs from b87733a4 only in AGENTS.md (+47).
• main CI on 1482b90e: verify, push event, run 41480334252, is green. 25 jobs passed, and 1 (A42 exclusion (${{ matrix.part }})) was skipped by its condition.

The proof-placement and logical-independence rule is now in force. Main's compliance remains an open correction obligation under MI-1 (#1029).

---

Generated by Claude Code