backlog(B-0715): file Soraya round-52 hand-off — register IsTimeInvariant axiom (DBSP chain rule)#4790
Merged
AceHack merged 1 commit intoMay 23, 2026
Conversation
…iant axiom in verification-registry Soraya's seventh autonomous routing tick (round 52, post-PR #4789 merge). tools/lean4/Lean4/DbspChainRule.lean:272 defines IsTimeInvariant as structure with commute_zInv : forall s n, f (zInv s) n = zInv (f s) n. This is a de facto axiom (no proof obligation; callers discharge per- operator). Both registered theorems (chain_rule_proposition_3_2 + Dop_LTI_commute) take it as hypothesis — but the axiom itself has no registry row. The artifact's own strikethrough revision history (Prop 3.5 -> Theorem 3.3 correction round 35, 2026-05-05) proves the drift class this row is designed to catch already fired empirically on THIS exact axiom. Registry rows are the structural prevention; currently missing for the axiom. Distinct from B-0709 (TLA+/Alloy portfolio coverage), B-0713 (Lean ImaginaryStack exploratory), B-0714 (TLA+ runnability). New axis: registered theorems depending on unregistered axiom in same artifact. Soraya routing: Lean 4 correct primary (structure-with-axiom is Mathlib idiomatic); cross-check NONE today (axiom is structural not pointwise; Z3/FsCheck inapplicable; paper-fidelity is human-grade registry-audit). Cost lives at REGISTRY axis, not TOOL axis. TLA+-hammer guard: N/A. Effort: S. Assignee: kenji. Acceptance: 1 new registry row + 2 back-pointer cross-refs from existing theorem rows' Preconditions-diff sections. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships immediately. Authored via git plumbing fallback.
AceHack
deleted the
otto/soraya-round52-b0715-istimeinvariant-axiom-registry-2026-05-23
branch
AceHack
added a commit
that referenced
this pull request
May 24, 2026
…n under-counted by 3 LSM Spine specs (#4791) * backlog(B-0716): file Soraya round-53 scope-correction — B-0709 enumeration under-counted by 3 LSM-tree Spine specs Soraya's eighth autonomous routing tick (round 53, post-PR #4790 merge). B-0709 (round 42) enumerated 11 unregistered specs. Round-53 re-audit identified 14 unregistered — B-0709 missed the LSM-tree Spine cluster (Spine.als + SpineAsyncProtocol.tla + SpineMergeInvariants.tla) with O'Neil 1996 LSM-paper anchor. Coverage ratio correction: 7/21 = 0.33 (worse than B-0709's claimed 0.52; correct direction — auditor surfacing latent debt including its own first-pass-incompleteness). NOT a duplicate of B-0709; explicit scope-correction sub-finding. P3 because B-0709 is already filed and Kenji owns the umbrella; integration-time cost of authoring 3 additional Spine rows alongside the 11 is near-zero. Routing: existing TLA+ for *.tla, Alloy for *.als (no tool change). Failure at registry layer, identical class to B-0709/B-0713/B-0715. TLA+-hammer guard: N/A. Effort: S (marginal cost over B-0709-as-filed: near-zero). P3. Assignee: kenji. Substrate-honest framing: auditor's own first-pass-incompleteness, surfaced by re-audit. Filing as scope-correction (not supersession) keeps B-0709 umbrella intact while pinning on-disk truth. The auditor surfacing the gap in its own earlier enumeration is the same discipline applied recursively. Per Aaron's 2026-05-23 21:30Z policy-flip: Otto auto-ships immediately. Authored via git plumbing fallback. * fix(PR #4791): MD032 blank-line + BACKLOG.md regen — mechanical only Addresses the 2 failing required checks (`lint (markdownlint)` + `check docs/BACKLOG.md generated-index drift`). Does NOT address the 2 unresolved review threads on the row's arithmetic — those need design-judgment + author resolution (see PR comment). Mechanical fixes: 1. MD032: added blank line between "Round-53 on-disk truth:" header text and the immediately-following bullet list at line 45 2. BACKLOG.md: regenerated via `BACKLOG_WRITE_FORCE=1 bun tools/backlog/generate-index.ts` NOT fixing here (out of mechanical scope): - Line 42 arithmetic contradictions ("20 - 5 = 15" stated as "11 unregistered" + "11 + 7 = 18 total" — three internally- inconsistent claims about same registry state). Author/Soraya needs to clarify intent + the 5-vs-7 registered ambiguity - Line 48 spec count: `tools/tla/specs/` actually contains 19 TLA+ specs (verified `ls tools/tla/specs/*.tla | wc -l`), not 16 as B-0716 claims. Downstream "= 21 artifacts total" + "14 unregistered" + "Ratio: 7/21 = 0.33" all chain from this base. Re-derivation needs full registry-membership-semantics pass that mechanical fix can't safely make in isolation Threads remain unresolved — see PR comment. Co-Authored-By: Claude <noreply@anthropic.com> * fix(B-0716): correct arithmetic + on-disk counts per Codex P2 + Copilot reviews - Codex P2 (line 42): denominator math was internally contradictory (20 - 5 = 15 vs "11 unregistered + 7 registered = 18"). Mixed file-counts with theorem-entry counts. - Copilot (line 49): claimed 16 TLA+ specs but tools/tla/specs/ holds 19 (BftConsensus, EngagementLiveness, RecursiveSignedSemiNaive among the 14 named). On-disk truth (file-level, uniform unit-of-measure): - 19 TLA+ + 3 Alloy + 2 Lean spec files (excl. Lean4.lean root) = 24 total artifacts - 6 registered files (5 TLA+ + DbspChainRule.lean) in the registry - 18 unregistered files; B-0709 enumerated 11; this row surfaces the 3 missed Spine specs; remaining 4 tracked under sibling rows Acceptance criteria #4 updated: 7/21=0.33 -> 6/24~=0.25 baseline. Verification commands run: ls tools/tla/specs/*.tla | wc -l # 19 ls tools/alloy/specs/*.als | wc -l # 3 find tools/lean4 -name '*.lean' # Lean4.lean, ToyModel.lean, # DbspChainRule.lean Co-Authored-By: Claude <noreply@anthropic.com> --------- Co-authored-by: Claude <noreply@anthropic.com>
This was referenced May 24, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Soraya autonomous round 52 — Lean axiom-registry hygiene gap.
tools/lean4/Lean4/DbspChainRule.lean:272definesIsTimeInvariantstructure withcommute_zInv : ∀ s n, f (zInv s) n = zInv (f s) n. This is a de facto axiom (no proof obligation; per-operator discharge). Both registered theorems (chain_rule_proposition_3_2+Dop_LTI_commute) take it as hypothesis — but the axiom itself has no registry row.Why now
The artifact's own strikethrough revision history (Prop 3.5 → Theorem 3.3 correction, round-35 2026-05-05) proves the drift class this row is designed to catch already fired empirically on THIS exact axiom. Registry rows are the structural prevention; currently missing for the axiom.
Distinct from prior session findings
.cfgrunnability — different tool + axis (runnability vs registry)This row: registered theorems depend on unregistered axiom in same artifact. New axis.
Routing decision
TLA+-hammer guard
N/A — registry-hygiene, not tool-routing.
Effort
S (one row + 2 back-pointers). Assignee: kenji.
Test plan