Skip to content

records(#1007): state the #1009 closure in the SUBSTATE README and census - #1201

Merged
amaybaum merged 1 commit into
mainfrom
records/substate-1009-closure-20261108
Nov 8, 2026
Merged

amaybaum merged 1 commit into
mainfrom
records/substate-1009-closure-20261108

Conversation

@amaybaum

@amaybaum amaybaum commented Nov 8, 2026 •

Copy link
Copy Markdown
Owner

Records-only forward correction (step S6 of the #1009 retirement). Independently reviewed by a model reviewer (not human): ACCEPT at b6abb983 (comment 6721493571). CI green at this head (run 42467487890).

Changes

Both lines stopped being true when #1009 closed. They are corrected forward, following the #1011 precedent (32c86955).

  1. continuous-substates/README.md:10.
  2. lean-manuscript-census.json:1704, in the note of the GradientLinkFlatness family.

Left as they are (packet §3):

Checks

  • The census JSON parses, and tools/lean_manuscript_census.py reports OK.
  • legacy_records_check.py: 303 records intact. Neither file is listed.
  • artifact_placement_check.py: OK.
  • v3_verifier.py --receipts: all 53 hold. Five receipts name the census in their governed paths. None freezes it, because it is not a record directory or a seal record.

Merge: conditionally approved by the owner (chat, 2026-11-08) at this exact head, after independent review, an unchanged current-base comparison and green applicable main CI.


Generated by Claude Code

…nsus

Step S6 of the #1009 retirement, under the owner decision #1007
c.6719788955 (amaybaum, chat 2026-11-08; S1-S7 under review gates).
#1009 closed unmerged at 2026-11-08T09:25:51Z; `research/substate-1`
is kept at 77482a8; open work is carried on #1007 c.6719791533.
Packet #1007 c.6719401889 §3, "Post-closure propagation".

- continuous-substates/README.md:10: "#1009 is an open draft" ->
  closed without merging, with the decision, kept branch head and
  carry-forward comment.
- lean-manuscript-census.json:1704 (GradientLinkFlatness family note):
  "draft PR #1009 (open)" -> "(closed unmerged by owner decision, ...)".

The four "draft/unmerged" lines the packet names stay literally true
and are not edited. No claim, proof, classification or status changes.

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

amaybaum commented Nov 8, 2026

Copy link
Copy Markdown
Owner Author

Independent review of the S6 records-only correction at b6abb983 (model reviewer, not human): ACCEPT

This review was completed before CI turned green, but it was not posted at the time; it is posted here verbatim. Current-base check (coordinator): git diff --stat origin/main...b6abb983 against main 45eea51d still shows exactly the two reviewed files (continuous-substates/README.md, lean-manuscript-census.json, +4/−3), and the head merges cleanly.

Review text (verbatim)
# Independent review — PR #1201, S6 records-only correction (#1009 closure)

- Object: branch `records/substate-1009-closure-20261108`, head `b6abb983594f29e214c8216304907bee9cd4a335`,
  parent `9c201475ba6fd8f341591d14dd8e88db2e2aaa90` (main). Draft PR **#1201**.
- Reviewer: independent; read-only. No posts, commits or pushes; no shallow fetch.

## Verdict: ACCEPT

The diff is the minimal correction the packet (#1007 c.6719401889 §3, "Post-closure propagation";
S6) and the owner decision (#1007 c.6719788955) call for. Both new statements are true, the tooling
holds, and no other line on `main` says #1009 is open. The two process notes below are not about the
diff and need no change to `b6abb983`.

## 1. Scope of the diff

`git diff --stat 9c201475 b6abb983`: 2 files, +4/−3. `git diff --check` is clean.

- `verification/programmes/substratum/continuous-substates/README.md`, lines 10–11 → 10–12: the sentence
  "#1009 is an open draft; nothing here is adopted from it." is replaced. The rest of the paragraph is
  unchanged; the extra line is only rewrapping.
- `verification/lean-manuscript-census.json:1704`: the note of the "SUBSTATE-1 pure-gradient gauge link
  negative control and two-slice inverse" (`GradientLinkFlatness`) family. Only "(open)" changes, to
  "(closed unmerged by owner decision, #1007 comment 6719788955; branch research/substate-1 kept at
  77482a8c)". Status (`kernel-only`), `manuscript: []` and the rest of the note are unchanged.

Nothing else changes. **Pass.**

## 2. Facts (checked through the GitHub API, 2026-11-08)

| Statement | Check | Result |
|---|---|---|
| #1009 closed without merging | `pulls/1009`: `state=closed`, `merged=false`, `merged_at=null`, `closed_at=2026-11-08T09:25:51Z`; still `draft=true` | true |
| branch `research/substate-1` kept at `77482a8c` | `branches/research/substate-1` → `77482a8c43d0570661694bd572849d36602ab73a` (= #1009 head sha); object present locally | true |
| owner decision #1007 c.6719788955 | exists, by `amaybaum`, 09:25:24Z. Quotes the owner verbatim: "Retirement — Close #1009 without merging"; "Keep `research/substate-1` at `77482a8c`" | true |
| open work carried on #1007 c.6719791533 | exists, 09:25:42Z: "Carry-forward record for #1009 … This comment is now the accountable home for its open work". It names both corrections, README:10 and census:1704 | true |
| "Nothing here is adopted from it" | the decision adopts nothing; the carry-forward says the closure "adopts nothing" | true |

The census's "draft PR #1009" stays accurate, since the API still reports `draft=true`. **Pass.**

## 3. Register (§A.27 / §A.30)

The precedent `32c86955` (#1011) states the external PR's standing parenthetically: "(#1011 closed
unmerged)". The new README sentence states the standing of an external object: closed unmerged, by
whose decision, where the branch is kept and where its open work is accounted for. The census mirrors
the precedent's parenthetical form. Neither text narrates the document's own revisions: there is no
"formerly", "no longer", "now" or "is not listed". The old assertion is removed, not qualified, and no
dated status note is added. The README's past tense, "was closed", could be stative ("#1009 is closed
unmerged") to match the precedent exactly. That is optional and not a defect: it reports an event of
the external PR, not of this document. **Pass.**

## 4. Census

- `json.load` parses.
- `python3 tools/lean_manuscript_census.py` exits 0: "OK (every cited identifier and path resolves …
  complete relative to the maintained registry)". 240 modules, 122 families.
- The edit changes only a note. It is not a theorem strengthening, so §A.35's same-commit supersession
  or anchor contract is not triggered.

**Pass.**

## 5. Governed paths, receipts and legacy records

- These five receipts name `verification/lean-manuscript-census.json` in their governed paths:
  A32, CMP-1, KTRANS-SEP-2, OI-PAIR-MAXCONE-1 and PRESERVE-INDUCT-1. This is confirmed by grep of
  `verification/receipts/`.
- Semantics. A `v3-governed-paths` block (spec `S7`) declares which paths a round's own execution and
  landing delta may change (landing conditions 1–3 on `Δ = delta(LB, Λ)`). After the receipt, the only
  immutability is `G13` (`tools/v3_verifier.py` `records_unchanged`), which covers the files under the
  round's record directory, derived from its `preregistration.md` path, and its seal record. The census
  is neither, and it is not in `legacy-records.json`. Editing it outside a round is therefore
  permitted. It has been edited outside rounds since those receipts, for example `68e69f2e`,
  `b4b8d67c`, `c44fae54` and `a025eb4e`.
- `python3 tools/v3_verifier.py --receipts b6abb983…` reports "RECEIPTS 53 receipt(s), all hold" and
  exits 0.
- `python3 tools/legacy_records_check.py b6abb983…` reports "self-test OK", then "LEGACY 303 record(s)
  in 75 closed namespace(s), all intact".
- `python3 tools/artifact_placement_check.py` reports OK.

**Pass.**

## 6. Completeness: other lines on `main` about #1009's standing

A `git grep` for `1009` at `b6abb983` found 121 hits. Excluding number collisions (arXiv ids, line
numbers, hashes, data values), none says #1009 is open, active or the place where work continues.

- **Literally true, left as is.** These are packet row 26:
  - `native-causal-interface.md:206` ("draft and unmerged");
  - `native-packet-operand-and-setting.md:228` ("draft/unmerged");
  - `native-random-setting-test.md:191` ("draft and unmerged");
  - `later-access-preregistration.md:423` ("remains draft").

  Since `draft=true` and `merged=false`, all four hold. Other "draft PR #1009" or "draft #1009"
  mentions are identification or provenance and are true for the same reason. Two examples are
  `observable-recurrence.md:6` and `observation-context-protocol.md:3`.
- `shared-gauge-pointer-candidate.md:74`, "Keep #1009 draft, no manuscript change, no merge …". This is
  a scope instruction of the unit and is satisfied by a closed draft. It is not a status claim. No
  change.
- `o-ret-routes-20261103/SOURCES.md:50,55` quote #1031's table text, which includes "Q1/Q7 open". These
  are quotations; no change.
- **Borderline: `observer-interface-obsmu-20261104/ANALYSIS.md:480`**, "whether they count is a question
  for O-SET's open definition (#1009)".
  - "Open" modifies O-SET's definition, not the PR. That definition remains open: the NC-1 definition
    round closed DEFINITION-OPEN, Q7 is "open" in c.6719791533, and Q1 now has only an owner *working*
    definition, "not a proof".
  - Q1 does not decide whether additive offsets count, which is the question at :480.
  - "(#1009)" is a tracker label. It points to where the definition round's record lives: #1009
    c.6559049909 and c.6559054643, which are PR comments only.
  - The line is therefore still true, and the packet classifies it as provenance (row 32, with :122 and
    :1245).
  - The label could later point to #1007 c.6719791533, the accountable home. The file belongs to #866
    (writer-866 / Codex), however, and #1169 item 3 bars cross-branch edits. The packet routes this
    through S7 ("a pointer for the O-SET row" for Codex on #866). It is correctly out of S6's scope; no
    change here.
- `observer-interface-source.md:198` ("NC-1's Q1/Q7 remain open") is G1, assigned exclusively to Codex
  on #866. It is outside S6.

**Pass.** No other line needs correction.

## Process notes (not about the diff; no change to `b6abb983`)

1. **CI is red, for environmental reasons.**
   - On `b6abb983` (run 42467487890), "Mathlib bridge" fails at "Install elan", with exit 127 in the
     later steps. "Lean kernel check" fails at "Report toolchain".
   - The same two jobs are red on `main` `9c201475` (push run 42466942962: "Report toolchain" and
     "Build"), and on #1200's head `3daf5fde`.
   - The diff cannot cause this. The release gate did not run in CI, though, so the local runs above are
     the only gate evidence. The PR's own condition, "review, green CI and a separate owner decision",
     needs a green re-run before merge approval is requested.
2. **Sequencing.**
   - The owner's execution sequence in c.6719788955 reads: prepare the G2 PR, "Independently review and
     CI-check that PR before requesting its separate merge approval. Then prepare the status
     corrections …".
   - #1201 was opened at 09:30:42Z, four minutes after #1200 (09:26:35Z). At review time #1200 has no
     review comments and red CI.
   - The two PRs are independent. #1200's head tree equals `9c201475`'s tree (`06ad084a…`), so either
     merge order leaves #1201's two lines intact.
   - Even so, the coordinator should request #1201's merge approval only after #1200's review and CI
     gate, or confirm with the owner that preparing S6 in parallel is acceptable.
   - The PR body's "authorizes steps S1–S7" omits the decision's qualifier, "subject to the sequencing
     and review gates below".

Generated by Claude Code

@amaybaum
amaybaum marked this pull request as ready for review November 8, 2026 12:52
@amaybaum
amaybaum merged commit b73acf3 into main Nov 8, 2026
124 of 130 checks passed
@amaybaum
amaybaum deleted the records/substate-1009-closure-20261108 branch November 8, 2026 12:52

amaybaum commented Nov 8, 2026

Copy link
Copy Markdown
Owner Author

Merge record: #1201, S6 of the #1009 retirement (owner-approved, chat, 2026-11-08)

The owner (amaybaum) approved this in chat with the coordinating session on 2026-11-08 (recorded at #1169 c.6721498625). The approval was for a normal merge at head b6abb983, after four conditions were met:

This is administrative status maintenance; it does not revive or validate NC-1.

Merged as b73acf38a7c60026b4b514cd9b5077e1419a9a1d, a merge commit whose parents are 13340732 (main after #1198) and b6abb983.

How each condition was met:

  • Independent review: ACCEPT at b6abb983, posted verbatim as records(#1007): state the #1009 closure in the SUBSTATE README and census #1201 c.6721493571.
  • Current-base comparison: exactly the two reviewed files, continuous-substates/README.md and lean-manuscript-census.json (+4/−3). Neither file was touched on main since the branch point. The merge is clean.
  • Main CI on 13340732: green, 25 succeeded and 1 skipped.
  • PR CI at the head: run 42467487890, green on attempt 5. The earlier attempts failed only at the elan installer download (HTTP 504).

Scope. Two lines now record that #1009 was closed unmerged, with its branch research/substate-1 kept at 77482a8c. No scientific status changed, and NC-1 stays rejected. Main's push CI is running and will be reported here.


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