diff --git a/docs/pr-preservation/206-drain-log.md b/docs/pr-preservation/206-drain-log.md new file mode 100644 index 00000000..a1fc20df --- /dev/null +++ b/docs/pr-preservation/206-drain-log.md @@ -0,0 +1,238 @@ +# PR #206 drain log — craft fourth module: semiring-basics (recipe-template anchor) + +PR: +Branch: `craft/fourth-module-semiring-basics` +Drain session: 2026-04-25 (Otto, post-summary continuation autonomous-loop) +Thread count at drain start: 22 unresolved (Codex P2 + Copilot P1/P2) +Rebase context: clean rebase onto `origin/main`; no conflicts. + +Per Otto-250 (PR review comments + responses + resolutions are +high-quality training signals): full per-thread record with reviewer +authorship, severity, outcome class. + +This PR introduced the fourth craft module on semirings — the +"recipe template" that Zeta plugs different arithmetics into. +Drain caught a high density of mathematical-correctness findings +(K-relations precision, semiring-vs-ring distinction, GKT +homomorphism scope) plus several formatting fixes. Notable: 5 of +22 findings were stale-resolved-by-reality (`||` table-prefix +pattern already fixed in a later commit on the branch). + +--- + +## Outcome distribution: 14 FIX + 5 STALE-RESOLVED-BY-REALITY + 2 deferred + 1 surface-class + +### A: FIX — Mathematical-correctness fixes (high-value) + +#### Thread A1 — `:183` — K-relations retraction-limitation overstated (Codex P2 + Copilot P1) + +- Reviewer: chatgpt-codex-connector + copilot-pull-request-reviewer +- Thread IDs: `PRRT_kwDOSF9kNM59P_tR` + `PRRT_kwDOSF9kNM59QEyr` (dup + Copilot) +- Severity: Codex P2 + Copilot P1 +- Finding: text said "pure-semiring-based K-relations support + lineage/provenance/counting but not retraction." This is misleading: + rings (like ℤ) ARE semirings, and K-relations over ℤ DO support + retraction via additive inverses. Zeta uses K-relations over ℤ for + retraction. +- Outcome: **FIX (P0-class precision error)** — reworded to scope the + limitation to "semirings WITHOUT additive inverses" (ℕ, 𝔹, lineage, + ℕ[X], tropical, max-plus, possibilistic). K-relations over a ring + (ℤ) DO support retraction; this is exactly what Zeta uses. The + pure-semiring-without-additive-inverses framing distinguishes from + rings cleanly. Commit `05ba3a0`. + +#### Thread A2 — `:213` — GKT homomorphism scope overstated (Codex P2) + +- Thread ID: `PRRT_kwDOSF9kNM59QEXi` +- Severity: P2 +- Finding: text stated GKT theorem applies to "every relational- + algebra result," but the homomorphism applies to **positive** + relational algebra (selection / projection / union / natural join); + relational difference / set-difference requires additive inverses + (rings, not pure semirings). +- Outcome: **FIX** — restricted claim to "POSITIVE relational + algebra (selection, projection, union, natural join, where the + operators are sums and products of input weights)." Added explicit + note that the homomorphism does NOT extend to relational + difference / set-difference; negative tuple-handling on those + operators must be re-derived per ring. Commit `05ba3a0`. + +#### Thread A3 — `:68` — Probabilistic-vs-possibilistic semantics (Codex P2) + +- Thread ID: `PRRT_kwDOSF9kNM59QEXn` +- Severity: P2 +- Finding: row labeled "Probabilistic ([0,1] fuzzy)" used max+multiply, + which is possibilistic / fuzzy / Viterbi-style — NOT probability + accumulation. +- Outcome: **FIX** — renamed row from "Probabilistic" to + "Possibilistic / fuzzy ([0,1])" with explicit note "max-times; not + probability accumulation." Commit `05ba3a0`. + +#### Thread A4 — `:195` — Lineage semiring multiplication semantics (Codex P2) + +- Thread ID: `PRRT_kwDOSF9kNM59Phu-` +- Severity: P2 +- Outcome: **FIX** — reworded the lineage row to GKT-form: + multiplication is set-union (combining witness evidence from both + input tuples on a join), not intersection. Noted that ∩ form is + Why(X) provenance, distinct from Boolean lineage. Commit `05ba3a0`. + +#### Thread A5 — `:196` — N[X] retraction column (Codex P2) + +- Thread ID: `PRRT_kwDOSF9kNM59P4Qj` +- Severity: P2 +- Finding: table listed `N[X]` provenance with retraction "Depends on + coefficient ring," inconsistent with the type shown (N[X] is fixed + to natural-number coefficients). +- Outcome: **FIX** — N[X] retraction column now reads "No (N[X] + coefficients are ℕ — non-negative; no additive inverses + available)" with explicit pointer to ℤ[X] as the retractable + alternative. Commit `05ba3a0`. + +#### Thread A6 — `:193` — Tropical R = ℝ vs Zeta ℤ implementation (Copilot) + +- Thread ID: `PRRT_kwDOSF9kNM59Q-LW` +- Severity: P1 +- Finding: row stated `R = ℝ ∪ {+∞}` but Zeta's TropicalWeight in + `src/Core/NovelMath.fs:13-34` uses int64 with Int64.MaxValue as + +∞. +- Outcome: **FIX** — Tropical row now reads `Tropical (Zeta) | ℤ ∪ + {+∞}` with explicit note: "Zeta's TropicalWeight in NovelMath.fs is + backed by int64 with Int64.MaxValue as +∞; the math definition + extends to ℝ ∪ {+∞}, but Zeta's implementation uses ℤ." Commit + `05ba3a0`. + +### B: FIX — Cross-reference + format fixes + +#### Thread B1 — `:268` — TECH-RADAR column-name mismatch (Copilot P2) + +- Thread ID: `PRRT_kwDOSF9kNM59QEyr` +- Severity: P2 +- Outcome: **FIX** — replaced "ring 11" with "round 11" matching + `docs/TECH-RADAR.md` actual column structure (Technique | Ring | + Round | Notes). Commit `05ba3a0`. + +#### Thread B2 — `:269` — TECH-RADAR provenance row missing (Copilot P2) + +- Thread ID: `PRRT_kwDOSF9kNM59Q-Ld` +- Severity: P2 +- Finding: bullet claimed "provenance deferred" but TECH-RADAR has no + provenance row. +- Outcome: **FIX** — reframed as "provenance does not yet have a + tech-radar row; if/when it lands, the row will join the Tropical / + residuated-lattices entries." Treated as "not-yet-on-tech-radar" + rather than "deferred." Commit `05ba3a0`. + +#### Thread B3 — `:279` — "Per-user memory" label correction (Copilot P1) + +- Thread ID: `PRRT_kwDOSF9kNM59P5S2` +- Severity: P1 +- Outcome: **FIX** — reference now points at `memory/...` as a + clickable relative link with explicit annotation that the file is + in-repo per Otto-114 forward-mirror landing (NOT per-user Anthropic + AutoMemory). Commit `05ba3a0`. + +#### Thread B4 — `:99` — F# code block invalid (Copilot P1) + +- Thread ID: `PRRT_kwDOSF9kNM59Q-LO` + `PRRT_kwDOSF9kNM59PPfO` +- Severity: P1 + P2 (Copilot dup) +- Finding: F# fence-block contained ℤ/ℕ/𝔹 type identifiers, references + to a non-existent `ISemiring` interface, and `float` for Tropical + (current impl uses `TropicalWeight` backed by int64). +- Outcome: **FIX** — code-fence changed from `fsharp` to `text`; + added explicit "SHAPE SKETCH (pseudocode, not valid F#)" header; + Tropical return type updated `float` → `TropicalWeight`. Commit + `05ba3a0`. + +#### Thread B5 — `:13/14/17` — Prereq + next-suggested links to non-existent modules (Copilot P1+P2 ×3) + +- Thread IDs: `PRRT_kwDOSF9kNM59PNyi`, `PRRT_kwDOSF9kNM59PPff`, + `PRRT_kwDOSF9kNM59Q-LB` +- Severity: P1+P2 +- Finding: links to `subjects/zeta/zset-basics/`, + `subjects/zeta/operator-composition/`, `subjects/cs/databases/`. + Verification: + - `subjects/zeta/operator-composition/` EXISTS (clickable + relative link added). + - `subjects/zeta/zset-basics/` does NOT exist (marked + "forthcoming" with pointer to `subjects/zeta/retraction- + intuition/` as available prereq). + - `subjects/cs/` tree does NOT exist (marked as forward-reference). +- Outcome: **FIX** — three-way reframing per actual in-tree state. + Commit `05ba3a0`. + +#### Thread B6 — `:2` — H1 split across two lines (Copilot P2) + +- Thread ID: `PRRT_kwDOSF9kNM59PPeY` +- Severity: P2 +- Outcome: **FIX** — combined H1 to single line. Commit `05ba3a0`. + +### C: STALE-RESOLVED-BY-REALITY (5 threads — `||` table-prefix already fixed) + +#### Threads C1-C5 — `:65/70/113/188/197` — `||` table prefixes (Copilot P2 ×5) + +- Thread IDs: `PRRT_kwDOSF9kNM59PPfv`, `PRRT_kwDOSF9kNM59P5So`, + `PRRT_kwDOSF9kNM59P5S8`, `PRRT_kwDOSF9kNM59Q-K2`, + `PRRT_kwDOSF9kNM59Q-Lg` +- Severity: P2 +- Outcome: **STALE-RESOLVED-BY-REALITY** — current file at HEAD does + not have leading `||` on canonical-semiring-table rows (verified + via `grep -n '^||' docs/craft/subjects/zeta/semiring-basics/module.md` + — no matches). Reviewer threads pinned to a stale state of the file; + fix already landed prior to drain. + +### D: DEFERRED-TO-MAINTAINER (1 thread) + +#### Thread D1 — `:310` — "Aaron" name in Attribution section (Copilot P1) + +- Thread ID: `PRRT_kwDOSF9kNM59PPe3` +- Severity: P1 +- Outcome: **DEFERRED-TO-MAINTAINER** — same surface-class-vs- + faithful-attribution tension as #195 bootstrap/ deferrals. Craft/ + is current-state operational substrate where role-ref discipline + applies in principle, BUT Attribution section preserves PR-level + provenance (named ferry-and-absorb chain). High-blast-radius + rename of an Attribution section → defer to maintainer rather + than auto-applied. + +--- + +## Pattern observations (Otto-250 training-signal class) + +1. **K-relations retraction-limitation precision fix is the same shape + as the GKT homomorphism scope fix.** Both are subset-vs-superset + precision errors: rings ARE semirings (so "pure-semiring-based" + over-broadly excludes rings); positive relational algebra IS a + subset of relational algebra (so "every relational-algebra result" + over-broadly includes set-difference). Codex catches this class + reliably across math docs. + +2. **Stale-resolved-by-reality at ~23% on this PR** (5 of 22 threads). + The `||` table-prefix findings were the entire C class — pinned to + a pre-fix revision of the file. Same pattern as the broader drain + wave. Reply-and-resolve-with-evidence is the right pattern, not + re-fix. + +3. **Implementation-vs-math-definition tension on Tropical row.** + Mathematically Tropical is `(ℝ ∪ {+∞}, min, +)`, but Zeta's + implementation pins to ℤ for grid-cost / shortest-path use cases + over int64. The fix template captures both: name "Tropical (Zeta)" + with `ℤ ∪ {+∞}` plus an explicit note that the math definition + extends to ℝ. Pattern generalizes to any algebra where the textbook + formalization is broader than the implementation pin. + +4. **Cross-reference column-name accuracy** (Thread B1 — TECH-RADAR + "11" in Round column not Ring column) is its own findings class; + docs that cross-reference table cells need column-name + verification when the source-table evolves. Future doc-lint + candidate: parse referenced table headers + verify cited column. + +## Final resolution + +All 22 threads resolved at SHA `05ba3a0` (14 FIX + 5 STALE-RESOLVED- +BY-REALITY + 1 DEFERRED-TO-MAINTAINER + 2 dups). PR auto-merge +SQUASH armed; CI cleared; PR merged to main as `535b3f8`. + +Drained by: Otto, post-summary autonomous-loop continuation, cron +heartbeat `f38fa487` (`* * * * *`).