fix(b-0197): correct DBSP Prop 3.5 → Theorem 3.3 misattribution + close (6th cycle close-row)

docs/BACKLOG.md

@@ -517,7 +517,7 @@ are closed (status: closed in frontmatter)._
 - [ ] **[B-0194](backlog/P2/B-0194-incremental-auto-dispatcher-bilinear-capability-detection-aaron-2026-05-05.md)** IncrementalAuto dispatcher + checkBilinear law + capability detection (active-patterns over reflection) -- contract-by-convention gap in the algebra-capability system (Aaron 2026-05-05)
 - [ ] **[B-0195](backlog/P2/B-0195-dbsp-chain-rule-finding-cross-check-and-writeup-decision-aaron-2026-05-05.md)** DBSP chain rule formal-verification finding -- cross-check counter-example + verify Prop 3.5 reading + writeup decision (Aaron 2026-05-05)
 - [ ] **[B-0196](backlog/P2/B-0196-bigint-and-bignumber-integration-aaron-2026-05-05.md)** BigInt + BigRational + BigDecimal + BigFloat integration -- substrate survey + per-class adoption recommendation (Aaron 2026-05-05)
-- [ ] **[B-0197](backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md)** Lean DbspChainRule + chain-rule-proof-log -- correct Prop 3.5 misattribution to Theorem 3.3 (Aaron 2026-05-05)
+- [x] **[B-0197](backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md)** Lean DbspChainRule + chain-rule-proof-log -- correct Prop 3.5 misattribution to Theorem 3.3 (Aaron 2026-05-05)
 - [ ] **[B-0206](backlog/P2/B-0206-claude-code-env-mapping-skill-with-carved-sentences-references-ts-files-aaron-2026-05-05.md)** Claude Code environment-mapping skill with carved-sentences-in-behavior referencing existing capability-maps + our TS files
 - [ ] **[B-0208](backlog/P2/B-0208-launchd-forward-tick-reliability-merge-into-heartbeat-2026-05-06.md)** Launchd forward-tick reliability — merge forward logic into working heartbeat tick OR fix StartInterval for new services
 - [ ] **[B-0209](backlog/P2/B-0209-remote-only-background-agent-test-matrix-and-model-scouting-2026-05-06.md)** Remote-only background agent test matrix — prove claim coordination without local broadcast

docs/backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md

@@ -1,13 +1,13 @@
 ---
 id: B-0197
 priority: P2
-status: open
+status: closed
 title: Lean DbspChainRule + chain-rule-proof-log -- correct Prop 3.5 misattribution to Theorem 3.3 (Aaron 2026-05-05)
 tier: hygiene+correctness
 effort: S
 ask: PR #1593 cross-check finding -- the "Prop 3.5 unspoken precondition" framing is misattributed; arXiv:2203.16684 has no Proposition 3.5; the closest candidate (Theorem 3.3 "for an LTI operator Q we have Q^Delta = Q") states time-invariance EXPLICITLY in its statement, contradicting the Lean header's "unspoken premise" / "smuggled in as a convention" prose.
 created: 2026-05-05
-last_updated: 2026-05-05
+last_updated: 2026-05-16
 depends_on: []
 composes_with: [B-0195]
 tags: [lean, formal-verification, dbsp, citation-correction, hygiene]
@@ -243,3 +243,22 @@ because the cleanup is mechanical (text edits + revision
 notes) while B-0195's outstanding work is the writeup-format
 decision (which this row's finding now informs but does not
 replace).
+
+## Resolution
+
+Closed 2026-05-16 via #2-Ready pickup. Row had embedded mechanical
+grep falsifier; work was bounded and ready-to-do.
+
+**Text corrections shipped** (3 bare misattributions replaced):
+
+- `tools/lean4/Lean4/DbspChainRule.lean` line 51 — strikethrough + `[corrected 2026-05-05: Theorem 3.3]`
+- `tools/lean4/Lean4/DbspChainRule.lean` line 203 — same correction pattern
+- `docs/research/chain-rule-proof-log.md` lines 113-114 — same correction pattern
+
+Each correction cites Theorem 3.3 ("Q^Delta = Q for LTI operators") explicitly.
+
+**Falsifier passes** — row's embedded two-pass grep returns 0 bare references after this PR.
+
+**Note on anchor date**: row's falsifier uses `[corrected 2026-05-05:` exact tag (the date the misattribution was first identified via PR #1593 cross-check). Fixed on 2026-05-16 but using row-anchored tag for falsifier compatibility.
+
+**Composes with**: this row was catalogued as #2-Ready in [memory/feedback_audit_backlog_status_drift_sub_class_catalog_otto_cli_2026_05_16.md](../../../memory/feedback_audit_backlog_status_drift_sub_class_catalog_otto_cli_2026_05_16.md) — the first instance that named the sub-class. This close-row vindicates the catalog's prediction: #2-Ready rows are pickup candidates for budget-healthy ticks.

docs/research/chain-rule-proof-log.md

@@ -110,9 +110,9 @@ Neither axiom closes B2. The failure cases were:
    group-homomorphism axiom at the stream level forces this.
 
 B2 is the statement that linear stream operators *commute with
-delay*. At the DBSP paper level this is smuggled in as a
-convention (Budiu et al. Proposition 3.5 uses it without
-naming it); in Lean it must be an explicit part of the contract.
+delay*. At the DBSP paper level this is the LTI condition: ~~smuggled in as a~~
+~~convention (Budiu et al. Proposition 3.5 uses it without naming it)~~
+[corrected 2026-05-05: Budiu et al. Theorem 3.3 explicitly states `Q^Delta = Q` for LTI operators; the paper makes it explicit, not smuggled-in]; in Lean it must be an explicit part of the contract.
 
 ### Round-35 resolution — the hierarchy
 

tools/lean4/Lean4/DbspChainRule.lean

@@ -48,7 +48,7 @@ Round-35 landmarks:
 
 * B2 resolved from a conceptual wall into a contract field —
   `IsTimeInvariant` predicate, elevated to an axiom matching the
-  DBSP paper's unspoken premise (Budiu et al. Prop. 3.5).
+  DBSP paper's ~~unspoken premise (Budiu et al. Prop. 3.5)~~ LTI condition [corrected 2026-05-05: Theorem 3.3 states LTI explicitly; paper makes it explicit, formalization separates sub-properties].
 * B1 statement corrected — the earlier `f (fun _ => s k) k` form
   silently required pointwise-linearity; the generic linear-
   plus-time-invariant form is `f (I s) = I (f s)`.
@@ -199,8 +199,8 @@ commutation with delay. Three candidate upgrades were considered:
   commute with `zInv`.
 * **Time-invariance** — `f ∘ zInv = zInv ∘ f` as stream
   operators. This IS B2; adding it as an axiom closes B2
-  trivially. In DBSP literature this is the unspoken premise of
-  Budiu et al. Proposition 3.5.
+  trivially. In DBSP literature this corresponds to the LTI
+  condition: ~~unspoken premise of Budiu et al. Proposition 3.5~~ Budiu et al. Theorem 3.3 [corrected 2026-05-05: paper states `Q^Delta = Q` for LTI operators explicitly via Theorem 3.3, not in an unspoken premise].
 * **Pointwise action** — `f s n = φ (s n)` for some
   `AddMonoidHom φ`. Strong; implies both causal and time-
   invariant. But **disqualifies** the DBSP primitives: `I s n =