From a623ae5679211aa41c632a683baa3879427b181a Mon Sep 17 00:00:00 2001 From: Aaron Stainback Date: Sat, 23 May 2026 12:52:27 -0400 Subject: [PATCH] docs(backlog): update backlog files (decomposed from #4059) --- docs/BACKLOG.md | 4 +- ...-substrate-consistency-audit-2026-05-14.md | 20 ++-- ...e-and-imaginary-intersection-2026-05-16.md | 61 ++++++++++ ...tural-rewrite-soraya-handoff-2026-05-17.md | 110 ++++++++++++++++++ 4 files changed, 184 insertions(+), 11 deletions(-) create mode 100644 docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md create mode 100644 docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index 49339c175b..1a1fba8cf0 100644 --- a/docs/BACKLOG.md +++ b/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 diff --git a/docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md b/docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md index 84e6520752..ff3e407a66 100644 --- a/docs/backlog/P1/B-0475-axis3-prior-art-substrate-consistency-audit-2026-05-14.md +++ b/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 diff --git a/docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md b/docs/backlog/P2/B-0584-imaginary-stack-step-1-formalize-4d-cube-and-imaginary-intersection-2026-05-16.md new file mode 100644 index 0000000000..e5ecd5bea1 --- /dev/null +++ b/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. diff --git a/docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md b/docs/backlog/P2/B-0612-lean-imaginary-stack-toy-model-structural-rewrite-soraya-handoff-2026-05-17.md new file mode 100644 index 0000000000..2f4f479c65 --- /dev/null +++ b/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.