diff --git a/docs/BACKLOG.md b/docs/BACKLOG.md index a2ff20e13..8a5e0079c 100644 --- a/docs/BACKLOG.md +++ b/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 diff --git a/docs/backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md b/docs/backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md index 8753e8cf0..4c1b0ab7c 100644 --- a/docs/backlog/P2/B-0197-lean-prop-3-5-misattribution-cleanup-aaron-2026-05-05.md +++ b/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. diff --git a/docs/research/chain-rule-proof-log.md b/docs/research/chain-rule-proof-log.md index 4a3121527..e74ffa753 100644 --- a/docs/research/chain-rule-proof-log.md +++ b/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 diff --git a/tools/lean4/Lean4/DbspChainRule.lean b/tools/lean4/Lean4/DbspChainRule.lean index 868b20dcf..921115781 100644 --- a/tools/lean4/Lean4/DbspChainRule.lean +++ b/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 =