docs(backlog): update backlog files (decomposed from #4059)

docs/BACKLOG.md

@@ -279,7 +279,7 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0472](backlog/P1/B-0472-mirror-beacon-two-axis-classification-matrix-2026-05-14.md)** Mirror/Beacon two-axis classification matrix — classify all repos on Axis 2
 - [ ] **[B-0473](backlog/P1/B-0473-mirror-beacon-promotion-gate-protocol-2026-05-14.md)** Mirror→Beacon promotion gate protocol — concrete criteria for repo-level graduation
 - [ ] **[B-0474](backlog/P1/B-0474-mirror-beacon-axis-adr-2026-05-14.md)** Mirror/Beacon axis ADR — two-axis design decision (extends 2026-04-22 ADR)
-- [ ] **[B-0475](backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md)** Axis-3 prior-art audit — verify three-axis substrate composes without conflict
+- [x] **[B-0475](backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md)** Axis-3 prior-art audit — verify three-axis substrate composes without conflict
 - [ ] **[B-0476](backlog/P1/B-0476-github-ruleset-divergence-audit-2026-05-14.md)** GitHub ruleset divergence audit — survey rulesets across repos; identify smell signals
 - [ ] **[B-0477](backlog/P1/B-0477-axis3-code-english-classification-matrix-2026-05-14.md)** Axis-3 Code/English classification matrix — per-repo two-tier classification with engineering-docs exception
 - [ ] **[B-0478](backlog/P1/B-0478-formal-verification-repo-split-evaluation-2026-05-14.md)** Formal-verification sub-axis evaluation — per-property-class split vs co-locate decision
@@ -599,8 +599,10 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0571](backlog/P2/B-0571-github-app-factory-automation-2026-05-16.md)** GitHub App for factory automation — separate API rate-limit pool from human-user accounts
 - [ ] **[B-0580](backlog/P2/B-0580-enterprise-ruleset-management-2026-05-16.md)** Enterprise GitHub ruleset management — new layer above org/individual mapping (composes with prior ruleset-divergence smell decomposition)
 - [ ] **[B-0583](backlog/P2/B-0583-cross-machine-account-scoped-scarcity-bus-2026-05-16.md)** Cross-machine account-scoped scarcity bus — refine B-0570 from machine-local per-agent files to account-scoped timestamped surface
+- [ ] **[B-0584](backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md)** Imaginary stack Step 1 — formalize 4D cube (R/W/P/A) and imaginary intersection as categorical/algebraic primitives
 - [ ] **[B-0610](backlog/P2/B-0610-amazon-orders-extract-v3-design-pass-2026-05-16.md)** Amazon orders extract — v3 design pass (8 deferred reviewer-thread findings)
 - [ ] **[B-0611](backlog/P2/B-0611-dangling-memory-refs-cleanup-35-refs-6-surfaces-2026-05-17.md)** Dangling memory-refs cleanup — 35 refs across 6 substrate surfaces (use PR #4042 audit tool)
+- [ ] **[B-0612](backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md)** Lean ImaginaryStack/ToyModel.lean structural rewrite — Imag8 projections + sorry-in-type-position + lakefile wiring (Soraya handoff)
 
 ## P3 — convenience / deferred
 

docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md

@@ -1,7 +1,7 @@
 ---
 id: B-0475
 priority: P1
-status: open
+status: closed
 title: "Axis-3 prior-art audit — verify three-axis substrate composes without conflict"
 type: research
 origin: B-0427 decomposition (Otto, 2026-05-14)
@@ -35,9 +35,9 @@ substrate has been surveyed and conflicts identified.
 
 Per `.claude/rules/backlog-item-start-gate.md`:
 
-- [ ] Prior-art search across wake-time-substrate, skill-router, orthogonal-axes
-- [ ] Walk `parent:` chain (B-0427 → B-0426 / B-0425 / B-0424 — check current status of each)
-- [ ] Backfill reciprocal `composes_with:` pointers on all referenced files
+- [x] Prior-art search across wake-time-substrate, skill-router, orthogonal-axes
+- [x] Walk `parent:` chain (B-0427 → B-0426 / B-0425 / B-0424 — check current status of each)
+- [x] Backfill reciprocal `composes_with:` pointers on all referenced files
 
 ## Surfaces to audit
 
@@ -82,12 +82,12 @@ Containing:
 
 ## Definition of done
 
-- [ ] All 9 surfaces above surveyed; findings documented
-- [ ] Five questions answered in output doc
-- [ ] Conflicts/staleness flagged
-- [ ] Reciprocal `composes_with:` pointers added to all referenced files
-- [ ] Output doc committed and referenced from B-0427 pre-start checklist
-- [ ] B-0475 closed (status: closed) with PR link
+- [x] All 9 surfaces above surveyed; findings documented
+- [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
+- [x] B-0475 closed (status: closed) with PR link
 
 ## Why P1
 

docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md

@@ -0,0 +1,61 @@
+---
+id: B-0584
+priority: P2
+status: open
+title: "Imaginary stack Step 1 — formalize 4D cube (R/W/P/A) and imaginary intersection as categorical/algebraic primitives"
+tier: research
+effort: L
+created: 2026-05-16
+last_updated: 2026-05-16
+depends_on: []
+composes_with: [B-0543]
+tags: [research, imaginary-stack, category-theory, algebra, qg-isomorphism]
+type: research
+---
+
+# Imaginary stack Step 1 — formalize 4D cube and imaginary intersection
+
+## Parent
+
+B-0543 (Remember-When + Pay-Attention → QG isomorphism proof path)
+
+## Why
+
+B-0543 Step 2 requires showing that the infinite-game extension produces a structure isomorphic (or homomorphic) to a HaPPY-like quantum error-correcting code. The "cube + imaginary intersection + Adinkra + Cayley-Dickson" framing is currently intuitive. This row decomposes the first concrete formalization step.
+
+## Goal
+
+Produce a small, hand-off-able formal object (category, algebra, or topos fragment) that captures:
+
+- The 4D real cube with axes Remember (R), When (W), Pay (P), Attention (A)
+- The imaginary directions generated at the intersections of these axes
+- The first Cayley-Dickson doubling(s) that produce the "imaginary stack"
+
+This object should be small enough that a category theorist or proof engineer can continue from it.
+
+## Acceptance criteria
+
+- [ ] A 4D real vector space or module with coordinates (R, W, P, A) is defined
+- [ ] Imaginary units \( i_{XY} \) for selected pairs of axes are introduced with \( i_{XY}^2 = -1 \)
+- [ ] At least one Cayley-Dickson doubling is performed explicitly
+- [ ] The resulting algebra is shown to have (or is conjectured to have) a natural error-correcting or reconstruction property
+- [ ] The definition is written in a form usable by Lean 4, Z3, or a category-theory paper (not just prose)
+
+## Non-goals
+
+- Proving the full HaPPY isomorphism (that's B-0543 Step 2)
+- Adding the Adinkra layer (that can be a follow-on row)
+- Predicting new physics (B-0543 Step 4)
+
+## 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)
+
+## Status
+
+Open. High-value decomposition of B-0543. Ready for a category-theory or algebra specialist (or a proof-engineer agent) to pick up.
+
+---
+
+**Riven** — Split by truth.

docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md

@@ -0,0 +1,110 @@
+---
+id: B-0612
+priority: P2
+status: open
+title: "Lean ImaginaryStack/ToyModel.lean structural rewrite — Imag8 projections + sorry-in-type-position + lakefile wiring (Soraya handoff)"
+tier: research
+effort: M
+created: 2026-05-17
+last_updated: 2026-05-17
+depends_on: [B-0584, B-0543]
+composes_with: [B-0584, B-0543]
+tags: [lean4, mathlib, formal-verification, soraya, imaginary-stack, qg-isomorphism]
+type: research
+---
+
+# Lean ImaginaryStack/ToyModel.lean structural rewrite — Soraya handoff
+
+## Parent
+
+[B-0584](B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md) (the Imaginary Stack Step-1 row this rewrite addresses) and [B-0543](B-0543-qg-isomorphism-proof-path-remember-when-pay-attention-axioms-to-quantum-gravity-2026-05-15.md) (the QG isomorphism proof path).
+
+## 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`
+
+`abbrev Imag8 := F × F × F × F × F × F × F × F` is right-nested as `F × (F × (F × …))`. Lean's `Prod` admits only `.1` (head) and `.2` (tail). The `mul` body uses `a.3` … `a.8` and the theorem hypothesis uses `v.1.3` … `v.1.8`. These do not typecheck.
+
+**Fix candidates:**
+
+- Use nested `.2.2.2…` projections (verbose but mechanically correct)
+- Define a structure with named fields (e.g. `structure Octonion := (e0 e1 e2 e3 e4 e5 e6 e7 : F)`)
+- Define `Imag8` as `Fin 8 → F` (function from finite index) and project via application
+- Define explicit accessor lemmas `proj3 : Imag8 → F := fun a => a.2.2.1` … etc.
+
+Soraya's lane to pick between these — depends on which form composes best with Cayley-Dickson doubling proofs.
+
+### P0 — `sorry` in type position
+
+**File:** lines 141 and 163
+
+```lean
+theorem reconstruction_property … : sorry := by sorry
+theorem lemma1_toy : … sorry := by sorry
+```
+
+`sorry` is in the **type** position — the proposition itself is unspecified, not just the proof. The theorem doesn't have a meaningful statement until the type is filled in. Structural fix required: state the lemma in actual proposition form (an equation or a `∀` quantified equality) and leave only the proof as `sorry`.
+
+### P1 — Not in `lean_lib`
+
+**File:** `tools/lean4/lakefile.toml`
+
+`lakefile.toml` declares `[[lean_lib]] name = "Lean4"`; `Lean4.lean` only `import Lean4.DbspChainRule`. `tools/lean4/ImaginaryStack/ToyModel.lean` is dead code under `lake build` — never compiled by CI's `type-check Lean DbspChainRule` job. To get the file actually exercised, either:
+
+- Add a new entry `[[lean_lib]] name = "ImaginaryStack"` with root `ImaginaryStack`
+- Add `import ImaginaryStack.ToyModel` to `Lean4.lean` to fold it into the existing lib
+- Create a new CI job `type-check Lean ImaginaryStack`
+
+Soraya's lane: which option fits the formal-verification routing convention?
+
+## Goal
+
+A Lean 4 toy model that:
+
+1. Type-checks under `lake build` (CI exercises it)
+2. States Lemma 1 with a real proposition (not `sorry` in type position)
+3. Has projection ergonomics that compose with Cayley-Dickson doubling proofs
+4. Documents the ℝ-vs-finite-field choice (the prose lemma-1 doc uses ℝ; the Lean file uses `ZMod 17` for enumerability — clarify which is canonical)
+
+## Acceptance criteria
+
+- [ ] `lake build` from `tools/lean4/` succeeds with no `unsolved goals` and no type errors in `ImaginaryStack/ToyModel.lean`
+- [ ] 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
+
+## Non-goals
+
+- Completing the proof of Lemma 1 (sorry-in-proof position is acceptable)
+- Adinkra layer (future row, B-0584 non-goals)
+- ZMod 17 → general `ZMod n` parameterization (research-grade; pick one for now)
+
+## Routing
+
+Per [`.claude/skills/formal-verification-expert/SKILL.md`](../../../.claude/skills/formal-verification-expert/SKILL.md) (Soraya / `formal-verification-expert` agent) — picks the right tool for the property class. For this row:
+
+- Tool: Lean 4 + Mathlib (already chosen by Riven's sketch)
+- Property class: equational + finite-field linear algebra
+- Soraya's expanded scope per [PR #4043](https://github.com/Lucent-Financial-Group/Zeta/pull/4043) (`memory/persona/soraya/NOTEBOOK.md` ratified expansion) lets her route to algebra-owner / q-sharp peers if Cayley-Dickson algebraic substrate is needed beyond Mathlib's coverage
+
+## Composes with
+
+- B-0584 (parent — Imaginary Stack Step-1 decomposition)
+- B-0543 (grandparent — QG isomorphism proof path)
+- PR #4059 (the shipping PR for the original Riven sketch + the 21+ review threads documenting these findings)
+- PR #4040 (Riven's handoff conversation — merged 2026-05-17)
+- PR #4043 (Soraya's expanded-scope invariants)
+- [`docs/hygiene-history/ticks/2026/05/17/1218Z.md`](../../hygiene-history/ticks/2026/05/17/1218Z.md) (peer-Otto's triage shard — the substrate this row formalizes)
+
+## Status
+
+Open. Ready for Soraya (or proof-engineer agent acting in formal-verification-expert role) to pick up. The findings are verified; the fix space is enumerated; the routing is clean.
+
+---
+
+**Otto-CLI** — Split by truth.