diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index 537d8b88d..93c6849ae 100644 --- a/docs/BACKLOG.md +++ b/docs/BACKLOG.md @@ -122,7 +122,7 @@ are closed (status: closed in frontmatter)._ - [x] **[B-0268](backlog/P1/B-0268-canary-test-rules-autoload-verification-2026-05-08.md)** Verify .claude/rules/ auto-load — run canary test - [x] **[B-0269](backlog/P1/B-0269-extract-carved-sentences-from-claude-md-to-rules-2026-05-08.md)** Extract carved sentences from CLAUDE.md to .claude/rules/ - [x] **[B-0270](backlog/P1/B-0270-pm2-role-skill-definition-2026-05-08.md)** PM-2 role - skill definition + persona agent -- [ ] **[B-0271](backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md)** PM-2 role — first research pass on Zeta feature gaps +- [x] **[B-0271](backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md)** PM-2 role — first research pass on Zeta feature gaps - [ ] **[B-0272](backlog/P1/B-0272-atari-rom-canonical-naming-tosec-lookup-2026-05-08.md)** Atari 2600 ROM canonical naming via TOSEC/No-Intro hash lookup - [ ] **[B-0273](backlog/P1/B-0273-atari-rom-safe-unsafe-folder-split-2026-05-08.md)** Atari 2600 ROM safe/unsafe folder split for license compliance - [ ] **[B-0274](backlog/P1/B-0274-pages-astro-workflow-scaffold-and-sha-pinning-2026-05-08.md)** Pages discoverability - Astro workflow scaffold and SHA pinning @@ -225,12 +225,12 @@ are closed (status: closed in frontmatter)._ - [ ] **[B-0409](backlog/P1/B-0409-wallet-immune-system-vaccine-spread-poucc-spec.md)** Wallet immune system — vaccine spread + PoUW-CC gate + attack absorption spec - [ ] **[B-0418](backlog/P1/B-0418-amplification-ratio-metric-dashboard-2026-05-11.md)** Amplification ratio metric — human input : agent actions on dashboard - [ ] **[B-0419](backlog/P1/B-0419-honest-agenda-amplification-metric-aaron-2026-05-11.md)** Honest agenda amplification metric — actions weighted by agenda alignment -- [ ] **[B-0423](backlog/P1/B-0423-memory-md-serialization-point-2026-05-12.md)** MEMORY.md serialization-point anti-pattern -- [ ] **[B-0423.1](backlog/P1/B-0423.1-reindex-memory-md-test-coverage-collectentries-renderindex.md)** Extend reindex-memory-md.ts test coverage — collectEntries + renderIndex -- [ ] **[B-0423.2](backlog/P1/B-0423.2-memory-docs-update-heap-state-acceptable.md)** Update memory/ documentation to describe heap-state-acceptable model -- [ ] **[B-0423.3](backlog/P1/B-0423.3-wire-reindex-into-autonomous-loop-tick.md)** Wire reindex-memory-md.ts into autonomous-loop tick cadence -- [ ] **[B-0423.4](backlog/P1/B-0423.4-relax-memory-index-integrity-ci-check.md)** Relax memory-index-integrity.yml CI check — heap-state-acceptable -- [ ] **[B-0423.5](backlog/P1/B-0423.5-close-b0088-chain-superseded-by-heap-architecture.md)** Close B-0088 chain as superseded by B-0423 heap architecture +- [x] **[B-0423](backlog/P1/B-0423-memory-md-serialization-point-2026-05-12.md)** MEMORY.md serialization-point anti-pattern +- [x] **[B-0423.1](backlog/P1/B-0423.1-reindex-memory-md-test-coverage-collectentries-renderindex.md)** Extend reindex-memory-md.ts test coverage — collectEntries + renderIndex +- [x] **[B-0423.2](backlog/P1/B-0423.2-memory-docs-update-heap-state-acceptable.md)** Update memory/ documentation to describe heap-state-acceptable model +- [x] **[B-0423.3](backlog/P1/B-0423.3-wire-reindex-into-autonomous-loop-tick.md)** Wire reindex-memory-md.ts into autonomous-loop tick cadence +- [x] **[B-0423.4](backlog/P1/B-0423.4-relax-memory-index-integrity-ci-check.md)** Relax memory-index-integrity.yml CI check — heap-state-acceptable +- [x] **[B-0423.5](backlog/P1/B-0423.5-close-b0088-chain-superseded-by-heap-architecture.md)** Close B-0088 chain as superseded by B-0423 heap architecture - [ ] **[B-0424](backlog/P1/B-0424-three-repo-split-stage1-create-forge-ace-with-scaffolding-aaron-2026-05-13.md)** Three-repo split Stage 1 — create empty Forge + ace with day-one scaffolding - [ ] **[B-0425](backlog/P1/B-0425-product-repo-split-planning-ksk-wellness-american-dream-civsim-honor-system-no-fork-license-aaron-2026-05-13.md)** Product-repo split planning — KSK / wellness / civsim / AD2.0 / DIO / Aurora / Dawn — honor-system no-fork license - [ ] **[B-0426](backlog/P1/B-0426-repo-split-orthogonal-mirror-beacon-axis-aaron-2026-05-13.md)** Repo-split orthogonal Mirror/Beacon axis — speculative-fast-forks vs governance-citation-gated @@ -245,6 +245,8 @@ are closed (status: closed in frontmatter)._ - [ ] **[B-0440](backlog/P1/B-0440-standing-by-failure-mode-detector-background-service-2026-05-13.md)** Standing-by failure-mode detector — background service that catches idle-foreground + nudges via bus - [ ] **[B-0441](backlog/P1/B-0441-backlog-row-ready-to-grind-notifier-background-service-2026-05-13.md)** Backlog-row-ready-to-grind notifier — background service that proactively assigns claims when agent queue empty - [ ] **[B-0442](backlog/P1/B-0442-missed-substrate-cascade-detector-background-service-2026-05-13.md)** Missed-substrate cascade detector — background service that catches branch-vs-merged-PR drift (e.g., Otto-section-missed-PR-2980-by-3-min class) +- [ ] **[B-0444](backlog/P1/B-0444-getting-started-guide-for-library-consumers-pm2-2026-05-13.md)** Getting-started guide for Zeta library consumers — quickstart doc + sample project +- [ ] **[B-0445](backlog/P1/B-0445-csharp-fluent-operator-surface-pm2-2026-05-13.md)** C# fluent operator surface — Map, Filter, Join, Distinct, Window via idiomatic CSharp API ## P2 — research-grade @@ -343,9 +345,9 @@ are closed (status: closed in frontmatter)._ - [x] **[B-0081](backlog/P2/B-0081-path-gate-kotlin-scala-codex-pr-662.md)** codeql.yml path-gate should match `*.kt` + `*.scala` not just `*.java` — Codex P2 on PR #662 - [ ] **[B-0082](backlog/P2/B-0082-glossary-persona-name-attribution-role-ref-conversion-pr-671.md)** docs/GLOSSARY.md provenance entries use persona-name attribution; convert to role-refs - [x] **[B-0086](backlog/P2/B-0086-port-tools-hygiene-python-to-typescript-bun-aaron-2026-04-28.md)** Port tools/hygiene Python scripts to TypeScript/Bun (factory-default; AI/ML carve-out applies) -- [ ] **[B-0088](backlog/P2/B-0088-paired-edit-lint-advisory-not-enforcement-promote-to-required-check-otto-2026-04-28.md)** memory/MEMORY.md paired-edit lint is advisory only (not in required-status-checks); promote or remove the discoverability claim -- [ ] **[B-0088.1](backlog/P2/B-0088.1-verify-paired-edit-job-in-required-status-checks-riven-2026-05-11.md)** Verify whether `check memory/MEMORY.md paired edit` appears in required_status_checks.contexts or ruleset -- [ ] **[B-0088.2](backlog/P2/B-0088.2-decide-promote-vs-weaken-for-memory-paired-lint-riven-2026-05-11.md)** Maintainer decision gate — promote paired-edit lint to required or weaken its discoverability claim +- [x] **[B-0088](backlog/P2/B-0088-paired-edit-lint-advisory-not-enforcement-promote-to-required-check-otto-2026-04-28.md)** memory/MEMORY.md paired-edit lint is advisory only (not in required-status-checks); promote or remove the discoverability claim +- [x] **[B-0088.1](backlog/P2/B-0088.1-verify-paired-edit-job-in-required-status-checks-riven-2026-05-11.md)** Verify whether `check memory/MEMORY.md paired edit` appears in required_status_checks.contexts or ruleset +- [x] **[B-0088.2](backlog/P2/B-0088.2-decide-promote-vs-weaken-for-memory-paired-lint-riven-2026-05-11.md)** Maintainer decision gate — promote paired-edit lint to required or weaken its discoverability claim - [ ] **[B-0088.3](backlog/P2/B-0088.3-audit-memory-reference-existence-lint-advisory-status-riven-2026-05-11.md)** Audit memory-reference-existence-lint.yml for advisory-vs-required parity (same class as B-0088) - [ ] **[B-0088.4](backlog/P2/B-0088.4-audit-memory-index-duplicate-lint-advisory-status-riven-2026-05-11.md)** Audit memory-index-duplicate-lint.yml for advisory-vs-required parity - [ ] **[B-0088.5](backlog/P2/B-0088.5-audit-backlog-index-integrity-lint-advisory-status-riven-2026-05-11.md)** Audit backlog-index-integrity.yml for advisory-vs-required parity (B-0088 sibling) @@ -491,6 +493,8 @@ are closed (status: closed in frontmatter)._ - [x] **[B-0421](backlog/P2/B-0421-grok-peer-call-failure-cursor-agent-exit-1-2026-05-11.md)** Grok peer-call failure — cursor-agent exit 1 during multi-agent review - [ ] **[B-0430](backlog/P2/B-0430-peer-call-wrappers-codeql-insecure-tmp-file-all-8-wrappers-substrate-consistent-fix-2026-05-13.md)** Peer-call wrappers — CodeQL insecure-temp-file alert on autogenOutputPath() across all 8 wrappers (substrate-consistent fix needed) - [ ] **[B-0443](backlog/P2/B-0443-launch-substrate-carve-out-for-persona-naming-in-docs-launch-2026-05-13.md)** Launch-substrate carve-out — persona naming allowed in docs/launch/** under existing closed-list pattern +- [ ] **[B-0446](backlog/P2/B-0446-lean4-formal-proof-completion-dbsp-core-identities-pm2-2026-05-13.md)** Lean 4 formal proof completion — DBSP chain rule + core stream-calculus identities +- [ ] **[B-0447](backlog/P2/B-0447-nuget-package-metadata-completeness-pm2-2026-05-13.md)** NuGet package metadata completeness — description, tags, SourceLink, semantic versioning ## P3 — convenience / deferred diff --git a/docs/backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md b/docs/backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md index ffd8cab65..511be1a39 100644 --- a/docs/backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md +++ b/docs/backlog/P1/B-0271-pm2-first-research-pass-2026-05-08.md @@ -1,13 +1,13 @@ --- id: B-0271 priority: P1 -status: open +status: closed title: "PM-2 role — first research pass on Zeta feature gaps" created: 2026-05-08 -last_updated: 2026-05-08 +last_updated: 2026-05-13 parent: B-0145 depends_on: [B-0270] -classification: blocked-on-B-0270 +classification: ready-for-close decomposition: atomic type: friction-reducer --- @@ -20,5 +20,18 @@ signals, user patterns, or competitor analysis. ## Acceptance criteria -- Research doc at docs/research/ with 5+ predicted gaps -- Each gap linked to existing backlog item or new row filed +- Research doc at docs/research/ with 5+ predicted gaps ✅ +- Each gap linked to existing backlog item or new row filed ✅ + +## Completion note (2026-05-13) + +Research doc: `docs/research/2026-05-13-pm2-zeta-feature-gap-prediction-first-pass.md` + +6 gaps identified: + +- Gap 1 — Getting-started guide → **B-0444** (new P1) +- Gap 2 — C# fluent operator surface → **B-0445** (new P1) +- Gap 3 — Lean 4 formal proof completion → **B-0446** (new P2) +- Gap 4 — NuGet package metadata → **B-0447** (new P2) +- Gap 5 — Shadow CLI slices 3–5 → existing B-0431, B-0432, B-0433 (P0) +- Gap 6 — DBpedia / MDM demo → existing B-0428 (P1) diff --git a/docs/backlog/P1/B-0444-getting-started-guide-for-library-consumers-pm2-2026-05-13.md b/docs/backlog/P1/B-0444-getting-started-guide-for-library-consumers-pm2-2026-05-13.md new file mode 100644 index 000000000..c29e8e789 --- /dev/null +++ b/docs/backlog/P1/B-0444-getting-started-guide-for-library-consumers-pm2-2026-05-13.md @@ -0,0 +1,62 @@ +--- +id: B-0444 +priority: P1 +status: open +title: "Getting-started guide for Zeta library consumers — quickstart doc + sample project" +type: friction-reducer +origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 +created: 2026-05-13 +last_updated: 2026-05-13 +depends_on: [] +composes_with: [B-0154, B-0445] +tags: [consumer-ux, getting-started, quickstart, documentation, onboarding, csharp, samples] +--- + +# B-0444 — Getting-started guide for library consumers + +## PM-2 signal + +External .NET developers who land on the repo from NuGet or GitHub +encounter Budiu et al. VLDB'23 math in the second paragraph of the README. +No `docs/getting-started.md` exists. No "hello world" circuit example +appears before the operator catalogue. + +## What + +1. `docs/getting-started.md` — 5-step quickstart: + install → create circuit → map → step/tick → inspect output. + Target audience: C# developer unfamiliar with DBSP. +2. `samples/QuickStart/` — minimal standalone project (single `.csproj`) + that mirrors the quickstart doc and builds with `dotnet run`. +3. README badge / top-10-lines link pointing to the guide. + +## Why now + +The library is production-ready (0 warnings, 470+ tests, 25-round +stability window on residuated lattices + FastCDC). The entry path is +research-paper difficulty. Every consumer who bounces in the first 5 +minutes is a permanent loss. + +## Non-goals + +- Does not replace the operator catalogue. +- Does not add new operators. +- Does not touch the F# API surface. + +## Acceptance criteria + +- [ ] `docs/getting-started.md` exists with a working 5-step C# example. +- [ ] `samples/QuickStart/` builds and runs: `dotnet run --project samples/QuickStart`. +- [ ] README links to the guide within the first 10 lines. +- [ ] `dotnet build -c Release` 0 warnings after changes. + +## Kill criteria + +If the Aurora pitch / factory-demo consumer path (B-0437 or equivalent) +already produces a canonical "hello world" moment, subsume this row under +that and close here. + +## Composes with + +- B-0154 (GitHub Pages SEO — the guide should be discoverable via Pages) +- B-0445 (C# fluent operator surface — quickstart uses the fluent API when it ships) diff --git a/docs/backlog/P1/B-0445-csharp-fluent-operator-surface-pm2-2026-05-13.md b/docs/backlog/P1/B-0445-csharp-fluent-operator-surface-pm2-2026-05-13.md new file mode 100644 index 000000000..222e3d340 --- /dev/null +++ b/docs/backlog/P1/B-0445-csharp-fluent-operator-surface-pm2-2026-05-13.md @@ -0,0 +1,65 @@ +--- +id: B-0445 +priority: P1 +status: open +title: "C# fluent operator surface — Map, Filter, Join, Distinct, Window via idiomatic CSharp API" +type: feature +origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 +created: 2026-05-13 +last_updated: 2026-05-13 +depends_on: [] +composes_with: [B-0444] +tags: [csharp, api-surface, fluent, operator, consumer-ux, dotnet] +--- + +# B-0445 — C# fluent operator surface + +## PM-2 signal + +The README states "a surface that feels native to both F# and C#." +Current state: `src/Core.CSharp/` contains exactly one file (`Variance.cs`) +— declaration-site variance shims. All operators (`Map`, `Filter`, `Join`, +`Distinct`, `GroupBy`, `Window`) require F# discriminated-union idioms. +The C# sample in `samples/FactoryDemo.Api.CSharp/` calls the F# surface directly. + +## What + +1. `ZetaCircuitBuilder` — C# fluent class wrapping `Circuit` and `Op<'T>` + so consumers can write: + ```csharp + var result = circuit + .From(source) + .Map(x => x.Name) + .Filter(name => name.Length > 0) + .Distinct(); + ``` +2. Extension methods on `Op>` for common operators. +3. XML doc comments on all new public C# symbols (IntelliSense parity). +4. Rewrite `samples/FactoryDemo.Api.CSharp/` to use the new fluent API. + +## Why now + +The existing CSharp sample builds but uses raw F# discriminated unions, +which is non-idiomatic C#. The fluent API is the minimum viable C# surface +that makes the "native to both F# and C#" README claim true. + +## Non-goals + +- Does not change operator semantics. +- Does not rewrite the F# core. +- Does not need to cover every operator — the six core ones suffice for v1. + +## Acceptance criteria + +- [ ] `src/Core.CSharp/` contains fluent builder covering: Map, Filter, Join, + GroupBy, Distinct, Window (sliding). +- [ ] `samples/FactoryDemo.Api.CSharp/` rewrites its circuit construction + to use the new fluent API, not raw F# types. +- [ ] All public C# types have `` XML docs. +- [ ] `dotnet build -c Release` 0 warnings. +- [ ] New `tests/Core.CSharp.Tests/` tests cover the fluent API round-trips. + +## Kill criteria + +If Aurora / enterprise pitch explicitly targets F# only (no C# consumer), +defer to P2. diff --git a/docs/backlog/P2/B-0446-lean4-formal-proof-completion-dbsp-core-identities-pm2-2026-05-13.md b/docs/backlog/P2/B-0446-lean4-formal-proof-completion-dbsp-core-identities-pm2-2026-05-13.md new file mode 100644 index 000000000..7ce893c12 --- /dev/null +++ b/docs/backlog/P2/B-0446-lean4-formal-proof-completion-dbsp-core-identities-pm2-2026-05-13.md @@ -0,0 +1,63 @@ +--- +id: B-0446 +priority: P2 +status: open +title: "Lean 4 formal proof completion — DBSP chain rule + core stream-calculus identities" +type: feature +origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 +created: 2026-05-13 +last_updated: 2026-05-13 +depends_on: [] +composes_with: [] +tags: [lean4, formal-verification, proof, dbsp, chain-rule, identities, correctness] +--- + +# B-0446 — Lean 4 formal proof completion for DBSP core identities + +## PM-2 signal + +Academic reviewers and enterprise adopters want to cite Zeta as a +verified DBSP implementation. `proofs/lean/ChainRule.lean` is a stub +(no proof body). The four core identities are tested as F# property +tests but carry no formal proof certificate. TECH-RADAR has Lean 4 +on "Assess" since Round 10 with no promotion. + +## What + +1. Complete `proofs/lean/ChainRule.lean`: + - `D ∘ I = id` (differentiation cancels integration) + - `I ∘ D = id` (integration cancels differentiation) + These are the bijection identities; they establish Z-sets form a + group under the stream calculus. +2. Add `proofs/lean/LinearityRule.lean`: + - For linear Q: `Q^Δ = Q` (trivial incrementalization). +3. Wire `lake build` in `proofs/lean/` as a CI check (new GitHub + Actions step, not blocking the main .NET build gate). +4. Promote TECH-RADAR Lean 4 from Assess → Trial. +5. README "formally verified" badge after CI check is green. + +## Why now + +TECH-RADAR Lean 4 has been on "Assess" since Round 10 with no action. +The stub proof `ChainRule.lean` is a lying stub — it exists but proves +nothing. A complete proof of two identities is the minimum step to a +verified claim, independent of the heavier F* extraction track. + +## Non-goals + +- Does not prove every operator. +- Does not require a full Mathlib port. +- Does not block the F* extraction path (TECH-RADAR "Assess" — runs + in parallel). + +## Acceptance criteria + +- [ ] `proofs/lean/ChainRule.lean` contains a complete proof with no `sorry`. +- [ ] `proofs/lean/LinearityRule.lean` exists with a complete proof. +- [ ] CI runs `lake build` in `proofs/lean/` and the step is green. +- [ ] TECH-RADAR Lean 4 row updated: Assess → Trial. + +## Kill criteria + +If the F* extraction path (TECH-RADAR entry) ships first and covers the +same identities, subsume this row under that PR and close here. diff --git a/docs/backlog/P2/B-0447-nuget-package-metadata-completeness-pm2-2026-05-13.md b/docs/backlog/P2/B-0447-nuget-package-metadata-completeness-pm2-2026-05-13.md new file mode 100644 index 000000000..146508646 --- /dev/null +++ b/docs/backlog/P2/B-0447-nuget-package-metadata-completeness-pm2-2026-05-13.md @@ -0,0 +1,72 @@ +--- +id: B-0447 +priority: P2 +status: open +title: "NuGet package metadata completeness — description, tags, SourceLink, semantic versioning" +type: friction-reducer +origin: PM-2 gap-prediction pass (B-0271) 2026-05-13 +created: 2026-05-13 +last_updated: 2026-05-13 +depends_on: [] +composes_with: [B-0154] +tags: [nuget, package-metadata, discoverability, sourcelink, versioning, dotnet] +--- + +# B-0447 — NuGet package metadata completeness + +## PM-2 signal + +`Directory.Build.props` has `zeta contributors` but +no `PackageDescription`, `PackageTags`, `RepositoryUrl`, +`PackageLicenseExpression`, or `PackageVersion`. `dotnet pack` currently +produces a `.nupkg` with a blank description, no tags, and version `1.0.0` +baked in. A developer searching NuGet for "incremental streaming F#" +would not find Zeta. + +## What + +Add to `Directory.Build.props`: + +```xml + + Zeta — retraction-native incremental view maintenance for .NET. + An F# implementation of the DBSP algebra (Budiu et al., VLDB'23). + Streaming, reproducible, near-zero-allocation. + +dbsp;incremental;streaming;retraction;fsharp;dotnet;ivm +https://github.com/Lucent-Financial-Group/Zeta +https://github.com/Lucent-Financial-Group/Zeta +Apache-2.0 +``` + +Semantic versioning: drive `Version` from a `VERSION` file checked into +git root (e.g., `1.0.0-alpha.1`) so every `dotnet pack` produces a +deterministic version tied to source. + +SourceLink: add `Microsoft.SourceLink.GitHub` to `Directory.Packages.props` +and `true` in `Directory.Build.props` +so debugger source-navigation works for downstream consumers. + +## Why now + +The Aurora pitch (PR #2924) and B-0154 (GitHub Pages SEO) are preparing +the external-consumption story. A NuGet package with no description and +a static version looks abandoned and is invisible to search. + +## Non-goals + +- Does not require publishing to nuget.org yet. +- Does not change any F# or C# source code. + +## Acceptance criteria + +- [ ] `dotnet pack` produces a `.nupkg` with Description, Tags, + RepositoryUrl, LicenseExpression populated. +- [ ] `Version` is driven from a `VERSION` file, not hard-coded. +- [ ] `dotnet pack --include-symbols` produces a `.snupkg` with SourceLink. +- [ ] `dotnet build -c Release` 0 warnings after the change. + +## Kill criteria + +If NuGet publishing is explicitly WONT-DO before the Aurora pitch closes, +defer to P3 and note that decision in this row. diff --git a/docs/research/2026-05-13-pm2-zeta-feature-gap-prediction-first-pass.md b/docs/research/2026-05-13-pm2-zeta-feature-gap-prediction-first-pass.md new file mode 100644 index 000000000..244b3c7b8 --- /dev/null +++ b/docs/research/2026-05-13-pm2-zeta-feature-gap-prediction-first-pass.md @@ -0,0 +1,209 @@ +# PM-2 Feature-Gap Prediction — First Research Pass + + +**PM-2 role:** proactive gap-prediction before consumer friction. +**Sources checked:** README, TECH-RADAR, VISION, `src/Core/`, `src/Core.CSharp/`, +`Directory.Build.props`, `docs/backlog/P*/B-0*.md` (544 rows), recent PRs, +`samples/`, `proofs/`. +**Prior-art search:** ran before each gap; no duplicate rows found except where noted. + +--- + +## Gap 1 — No getting-started guide for library consumers + +### Product Bet + +- **User / moment:** external .NET developer who finds `Zeta.Core` on NuGet or GitHub + and wants to write their first incremental circuit. They land on the README and + encounter Budiu et al. VLDB'23 math in the second paragraph. +- **Signal:** `docs/getting-started.md` does not exist. The README's introductory + paragraphs target readers already familiar with DBSP theory. No "hello world" + circuit example appears before the operator catalogue. +- **Proposed slices:** + 1. `docs/getting-started.md` — 5-step quickstart: install → create circuit → map → + step/tick → inspect output. Targets a C# developer who has never heard of DBSP. + 2. `samples/QuickStart/` — minimal standalone project (single `.csproj`) that mirrors + the quickstart doc. + 3. Pin a "Getting Started" link in the top-level README badge row. +- **Why now:** every new consumer who bounces in the first 5 minutes is a permanent + loss. The library is production-ready (0 warnings, extensive tests, TECH-RADAR + stability notes) but the entry path is research-paper difficulty. The mismatch is + the gap. +- **Non-goals:** does not replace the operator catalogue; does not add new operators; + does not touch the F# API surface. +- **Acceptance criteria:** + - `docs/getting-started.md` exists with a working 5-step C# example. + - `samples/QuickStart/` builds and runs with `dotnet run`. + - README links to the guide within the first 10 lines. +- **Kill criteria:** if the Aurora pitch / factory-demo demo-path already covers this + consumer moment, promote that as the canonical quickstart instead of creating a + parallel doc. +- **New backlog row:** B-0444 + +--- + +## Gap 2 — C# operator surface covers only variance shims + +### Product Bet + +- **User / moment:** C# developer who prefers fluent-builder or extension-method style. + They open `Zeta.Core.CSharp` and find one file: `Variance.cs` — declaration-site + variant interfaces. Every operator (`Map`, `Filter`, `Join`, `Distinct`, `GroupBy`, + `Window`) requires F# idioms. +- **Signal:** `src/Core.CSharp/` contains exactly `Variance.cs`. The CSharp sample in + `samples/FactoryDemo.Api.CSharp/` builds against `Zeta.Core` (F# surface) directly. + No C#-idiomatic entry path exists for the core circuit-building API. +- **Proposed slices:** + 1. `ZetaBuilder` — a C# fluent class wrapping `Circuit` and the `Op<'T>` graph + so consumers can write `circuit.From(source).Map(...).Filter(...).Join(...)`. + 2. Extension methods on `Op>` for the most common operators. + 3. XML doc comments on all public C# symbols (IntelliSense parity with the F# surface). +- **Why now:** the README says "a surface that feels native to both F# and C#" — the + current state does not deliver on that claim for the operator layer. The CSharp sample + builds but uses the F# discriminated-union surface directly, which is awkward for + everyday C# style. +- **Non-goals:** does not rewrite the F# core; does not change operator semantics. +- **Acceptance criteria:** + - `samples/FactoryDemo.Api.CSharp/` rewritten to use the new C# fluent API, not + raw F# types. + - All operators covered: Map, Filter, Join, GroupBy, Distinct, Window (sliding). + - `dotnet build -c Release` 0 warnings. +- **Kill criteria:** if the Aurora pitch routes exclusively through F# (no C# consumer + target), defer to P2. +- **New backlog row:** B-0445 + +--- + +## Gap 3 — Core DBSP identities are executable tests, not formal proofs + +### Product Bet + +- **User / moment:** academic reviewer, potential enterprise adopter, or alignment + researcher who wants to cite Zeta as a verified implementation of DBSP. They + look for `proofs/` and find `ChainRule.lean` — a stub with no body. +- **Signal:** `proofs/lean/ChainRule.lean` is a stub. TECH-RADAR lists Lean 4 + + Mathlib as "Assess" (Round 10). The four core identities (`I ∘ D = D ∘ I = id`, + chain rule for composition, linearity `Q^Δ = Q`, bilinear join rule) are tested + as executable F# property tests but carry no formal proof certificate. +- **Proposed slices:** + 1. Complete `ChainRule.lean` — prove `D ∘ I = id` and `I ∘ D = id` for `ZSet`. + 2. `proofs/lean/LinearityRule.lean` — prove `Q^Δ = Q` for linear operators. + 3. Promote TECH-RADAR Lean 4 from Assess → Trial. + 4. README badge: "formally verified core identities." +- **Why now:** the TECH-RADAR has had Lean 4 on "Assess" since Round 10. The + stub proof has not progressed. The F* extraction path (TECH-RADAR "Assess" entry) + remains blocked on FastCdc off-by-one risk. A Lean-first proof of the core + stream-calculus identities is the lowest-effort step to a verified claim, independent + of the F* track. +- **Non-goals:** does not prove every operator; does not require full Mathlib port. +- **Acceptance criteria:** + - `ChainRule.lean` has a complete, checked proof (no `sorry`). + - CI runs `lake build` in `proofs/lean/` as a required check. + - TECH-RADAR Lean 4 promoted to Trial. +- **Kill criteria:** if the F* extraction path (TECH-RADAR entry) ships first and + covers the same identities, subsume this row under that. +- **New backlog row:** B-0446 + +--- + +## Gap 4 — NuGet package metadata is sparse + +### Product Bet + +- **User / moment:** developer searching NuGet for an incremental / streaming operator + library. They see `Zeta.Core` with author "zeta contributors" and a blank + `PackageDescription`. +- **Signal:** `Directory.Build.props` has `zeta contributors` but + no ``, ``, ``, ``, + or ``. `PackageVersion` is absent (defaults to `1.0.0` on every + build). This means the NuGet listing would have no description, no tags for search, + no source-link URL, and a static version. +- **Proposed slices:** + 1. Add `PackageDescription`, `PackageTags` (dbsp, incremental, streaming, retraction, + fsharp, dotnet), `RepositoryUrl`, `PackageLicenseExpression` to + `Directory.Build.props`. + 2. Wire semantic versioning: `Version` driven by a `VERSION` file or git tag. + 3. Add `SourceLink` (Microsoft.SourceLink.GitHub) for debugger source navigation. +- **Why now:** the library is at a state where external interest is realistic (Aurora + pitch active, B-0154 GitHub Pages SEO row open). A NuGet listing with no description + and no tags is invisible to search and looks abandoned. +- **Non-goals:** does not require publishing to NuGet.org yet; just ensures the metadata + is correct for when publishing happens. +- **Acceptance criteria:** + - `dotnet pack` produces a `.nupkg` with Description, Tags, RepositoryUrl populated. + - Version is driven by a file/tag, not hard-coded `1.0.0`. + - SourceLink verified by `dotnet pack --include-symbols`. +- **Kill criteria:** if NuGet publishing is explicitly deferred (WONT-DO) before Aurora + pitch, note that in the row and defer to P3. +- **New backlog row:** B-0447 + +--- + +## Gap 5 — Shadow CLI slices 3–5 are P0 but have no implementation owner + +### Product Bet + +- **User / moment:** developer using an IDE (VS Code / Rider) who wants Zeta's + shadow-mode autocomplete: the grey-text suggestion that accepts on Tab. This is + the killer consumer feature in B-0402. Without slices 3–5, the shadow observer + can detect key events (`outlet.ts` ✅) but cannot read IDE grey-text + (slice 3 — osascript) or provide a stable `zeta shadow --loop` entry point + (slice 4). +- **Signal:** B-0431 (slice 3 — macOS grey-text detection), B-0432 (slice 4 — CLI + `--loop` flag), B-0433 (slice 5 — distribution / demo packaging) are all P0 and + open as of 2026-05-13. `tools/shadow/` contains the applescript + (`detect-grey-text.applescript`) but no wiring to the shadow observer. +- **Proposed approach:** no new row needed — rows exist. But the PM-2 finding is that + these three slices together form a **feature-complete shadow mode** and should be + treated as a sprint unit, not separate atomic rows. The risk is that each slice gets + deferred individually, leaving shadow mode perpetually "almost done." +- **Why now:** the Aurora pitch and factory-demo consumer moment both converge on "show + the agent augmenting a real developer workflow." Shadow mode is the only Zeta feature + that is visibly different from existing IDEs. Every tick these slices are deferred, + the demo story weakens. +- **Non-goals:** does not add new shadow-mode capabilities; just completes the existing + design. +- **Acceptance criteria:** B-0431 + B-0432 + B-0433 all closed by the same PR cluster. +- **Existing rows:** B-0431, B-0432, B-0433 (no new row needed). +- **Recommendation:** group B-0431/B-0432/B-0433 as a sprint target; treat them as + blocked-together rather than individually deferrable. + +--- + +## Gap 6 — DBpedia / HKT-MDM canonical demo has no implementation yet + +### Product Bet + +- **User / moment:** potential enterprise customer evaluating Zeta for master-data + management. They ask "can I see this working against real data?" There is no running + demo. +- **Signal:** B-0428 (DBpedia via dotNetRDF + F# CE) was filed 2026-05-13 and is open. + The VISION document names "intellectual backup of earth" as the terminal purpose. + MDM (master data management) is the enterprise instantiation of that purpose. + Without a demo, the thesis is not demonstrable. +- **Proposed approach:** no new row needed — B-0428 exists and is unblocked. +- **Why now:** the Aurora pitch (PR #2924) references this demo. The pitch is live. + The demo does not exist. +- **Non-goals:** does not require the F# type provider path (that's deferred in B-0428). +- **Existing row:** B-0428. + +--- + +## Summary table + +| Gap | Type | New row | Existing row | Priority | +|-----|------|---------|-------------|----------| +| Getting-started guide | UX / adoption | B-0444 | — | P1 | +| C# fluent operator surface | API surface | B-0445 | — | P1 | +| Lean 4 formal proof completion | Verification | B-0446 | — | P2 | +| NuGet package metadata | Discoverability | B-0447 | — | P2 | +| Shadow CLI slices 3–5 | Feature-complete | — | B-0431, B-0432, B-0433 | P0 | +| DBpedia / MDM demo | Demo / adoption | — | B-0428 | P1 | + +--- + +## Methodology note + +Surface-first discipline: every gap was checked against the existing 544 backlog rows +before filing. New rows B-0444..B-0447 were verified as net-new coverage. Gaps 5 and 6 +point to existing rows rather than inflating the backlog.