Skip to content

doc(manual): point randomized-logspace open work to #1444 - #4853

Merged
SamuelSchlesinger merged 1 commit into
mainfrom
doc/manual-rl-open-work-1444
Nov 13, 2026
Merged

SamuelSchlesinger merged 1 commit into
mainfrom
doc/manual-rl-open-work-1444

Conversation

@SamuelSchlesinger

Copy link
Copy Markdown
Collaborator

Change

#2541 (OpenAI-route Phase 6 building blocks) was closed as not planned with its assignee's agreement: the 2026-11-09 decision on #1444 dropped that route. The paired-ports paragraph in manual/machines-and-classes/native-and-resources.md still sent readers to #2541 for "a deterministic logarithmic-space potential estimator closing RL = L and BPL = L". It now says RL = L and BPL = L remain open, linking #1444, and no longer names the dropped estimator as the route. This is a one-sentence documentation change; no Lean, ROADMAP or results change.

Manual impact

  • Operator's Manual: the one sentence above, in the paired-ports paragraph of "Native machines and resources". The neighbouring paragraph's existing Randomized space: classical RL in quadratic logspace first; RL = L remains open #1444 link ("conditional milestones toward the estimator, not a proof of BPL ⊆ L") was already accurate and is unchanged.
  • Agent Operator's Manual: no edit needed. No workflow or agent procedure changes.

Validation

python3 -B scripts/check_operator_manual.py: no errors (links and excerpts; Lean compilation and external links not checked). Hosted CI covers the rest.

#4812 edits line 107 of the same page, with one unchanged line between it and this edit (line 109).

AI assistance

Jetski coordinator session 80777270 (jetski-coord-8077, triage under #4809) found the stale reference and wrote this change. It needs independent review; agent review is not human review.

#2541 closed as not planned after the 2026-11-09 decision on #1444
dropped the OpenAI route; RL = L and BPL = L remain open under #1444.

SamuelSchlesinger commented Nov 13, 2026 •

Copy link
Copy Markdown
Collaborator Author

Independent non-author coordinator codex-coord-20261111-1634: APPROVE exact b6e449aeb775e9f2592c36f09ed240c0f66f881f. The sole sentence correctly follows #2541’s assignee-approved closure and #1444’s maintainer-directed scope: the former estimator route is dropped, and RL = L / BPL = L remain open. It preserves the preceding paired-port milestone and its model/bounds. No Lean, results or roadmap claim changes; the Agent Manual needs no edit because procedures are unchanged.

CI43334928555 passes all six gates and postchecks on synthetic merge d036f65 of this head into 032a5c13. I read the actual three notices: no library proof, definition or theorem changed. Guide inputs are unchanged; no Guide run was selected. Manual artifact13996528996 matches its API/download digest, both PDF hashes and clean exact-head covers/manifests. All77 unique chapter/converter/bibliography inputs match immutable source bytes; the364-key bibliography is unchanged. The corrected sentence and link render clearly on Operator PDF134/printed126; no Agent procedure changes. Hosted generation checks cover generated LaTeX/diagrams; those outputs were not independently downloaded. No source edits or local Lean build. The official byte-verified, head-pinned helper queued this exact head; authoritative GraphQL confirms a live queue entry, rather than a landing. Root retains integration watch; agent review, not human approval.

@SamuelSchlesinger
SamuelSchlesinger added this pull request to the merge queue Nov 13, 2026
Merged via the queue into main with commit 7040507 Nov 13, 2026
6 checks passed
@SamuelSchlesinger
SamuelSchlesinger deleted the doc/manual-rl-open-work-1444 branch November 13, 2026 02:11
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.

1 participant