diff --git a/.cursor/bin/riven-loop-tick.ts b/.cursor/bin/riven-loop-tick.ts index 25e891a234..f06036588f 100644 --- a/.cursor/bin/riven-loop-tick.ts +++ b/.cursor/bin/riven-loop-tick.ts @@ -208,8 +208,17 @@ function heartbeat(): void { const gate = run("agent", [ "chat", "--mode", "ask", - "--model", "grok-4-20", - `Twin-flame heartbeat gate (Riven adversarial-truth-axis). Read git status, recent commits, open PRs, claim branches. Report: main HEAD, open PR count, claim count, any drift, contradiction, or theatrical governance. Adversarial register — call out what's wrong, not what's fine. Brief.`, + "--model", "grok-4.3", + [ + "You are Riven, trajectory manager and adversarial-truth-axis reviewer.", + "This is an autonomous 15-minute cycle.", + "Read broadcasts first from ~/.local/share/zeta-broadcasts/{otto,vera,lior,riven}.md.", + "Walk assigned trajectories. Decompose only what you hit mid-stride.", + "Produce at least one concrete, actionable claim or small PR scope.", + "When blocked, create a specific research child the next pickup cannot dodge.", + "Write your status to ~/.local/share/zeta-broadcasts/riven.md at the end.", + "GitHub PR state and actual file contents are authoritative.", + ].join(" "), ], agentTimeoutMs); agentStatus = gate.status === 0 ? "ok" : `exit-${gate.status}`; diff --git a/docs/pr-discussions/PR-4772-docs-lean4-add-readme-ci-badge-closes-publication-readiness.md b/docs/pr-discussions/PR-4772-docs-lean4-add-readme-ci-badge-closes-publication-readiness.md new file mode 100644 index 0000000000..01315c0816 --- /dev/null +++ b/docs/pr-discussions/PR-4772-docs-lean4-add-readme-ci-badge-closes-publication-readiness.md @@ -0,0 +1,142 @@ +--- +pr_number: 4772 +title: "docs(lean4): add README + CI badge \u2014 closes publication-readiness gaps #1+#2 on Lean DBSP chain rule" +author: "AceHack" +state: "MERGED" +created_at: "2026-05-23T21:47:38Z" +merged_at: "2026-05-23T22:05:27Z" +closed_at: "2026-05-23T22:05:27Z" +head_ref: "otto/lean4-readme-publication-readiness-2026-05-23" +base_ref: "main" +archived_at: "2026-05-23T22:19:28Z" +archive_tool: "tools/pr-preservation/archive-pr.ts" +--- + +# PR #4772: docs(lean4): add README + CI badge — closes publication-readiness gaps #1+#2 on Lean DBSP chain rule + +## PR description + +## Summary + +Closes the two surface-level publication-readiness gaps named in Otto's audit of the Lean DBSP chain rule artifact earlier today, composing with the DBSP-publication arc Aaron set as direction. + +**Gap #1**: No project-local README explaining build, paper-mapping, contribution beyond paper, citation, reproducibility setup. +**Gap #2**: No visible CI badge pointing reviewers at the green `lean-proof.yml` workflow. + +Both gaps were pure surface work, not mathematical work. The artifact itself is already **A-with-CI-green-since-2026-05-17** (zero `sorry`/`admit`, full predicate hierarchy, Prop 3.2 + Thm 3.3 corollary both closed, paper-drift audit round-35 corrections documented in companion proof log). + +## README content + +- **Repository layout table** (lakefile / lean-toolchain / Lean4.lean library root / DbspChainRule.lean / ImaginaryStack) +- **Build instructions** (elan + `lake build`) +- **Paper-to-Lean theorem mapping table** (6 rows: Def 3.1 → `Qdelta`; Prop 3.2 → `chain_rule_proposition_3_2`; Thm 3.3 corollary → `Dop_LTI_commute`; Thm 2.22 → `I_D_eq`; fundamental theorem → `D_I_eq`; sec 4.2 → `I_zInv_eq`) +- **Predicate hierarchy table** with DBSP-primitive membership (`IsLinear` / `IsCausal` / `IsTimeInvariant` / `IsPointwiseLinear`) +- **Round-35 paper-drift audit substrate-honest provenance** — three corrections documented (rename `chain_rule` → `Dop_LTI_commute`; B1 statement fix; chain_rule statement fix with impulse counter-example) +- **Future-work pointer** (`chain_rule_poly` polymorphic extension) +- **Verification registry pointer** +- **CI workflow pointer** with SHA-pinning notes +- **BibTeX** for citing this artifact + for the Budiu et al. paper +- **Composes-with refs** to chain-rule-proof-log, verification-registry, proof-tool-coverage, verification-drift-auditor skill, formal-verification-expert agent (Soraya) + +## CI badge + +[![Lean Proof CI](https://github.com/Lucent-Financial-Group/Zeta/actions/workflows/lean-proof.yml/badge.svg?branch=main)](https://github.com/Lucent-Financial-Group/Zeta/actions/workflows/lean-proof.yml) + +## Composes with Soraya's findings + +This PR closes pub-readiness gaps #1 + #2 on the chain-rule artifact. **Round-43 finding (BP-16 cross-check via FsCheck + Z3) is gap #3** — the substantive correctness gap that gets the artifact from "A-with-CI single-tool" to "A-with-CI three-tool BP-16-compliant" (Soraya's words: "the line publication crosses"). That row is pending Aaron's file-pick. + +Companion-paper draft (substantive writing, not surface work) remains for later. + +## Commit + +5th plumbing-fallback PR this session (#4755 Ani extraction / #4761 PR-triage rule / #4762 canonical Step-1a / #4765 B-0709 Soraya hand-off). Dotgit saturation throughout the day; pure-substrate addition; new file only (no edits to existing canonical surfaces under peer contention). + +## Test plan + +- [x] README renders cleanly in GitHub preview (tables + BibTeX + badge) +- [x] All cross-reference links resolve (`../../docs/research/*`, `../../.claude/*`) +- [x] Paper-to-Lean mapping table verified against actual theorem names in `DbspChainRule.lean` +- [x] Predicate hierarchy table matches Section 3 of the artifact +- [ ] CI green +- [ ] Auto-merge fires + +## Reviews + +### COMMENTED — @chatgpt-codex-connector (2026-05-23T21:49:27Z) + + +### 💡 Codex Review + +Here are some automated review suggestions for this pull request. + +**Reviewed commit:** `322fc6403f` + + +
ℹ️ About Codex in GitHub +
+ +[Your team has set up Codex to review pull requests in this repo](https://chatgpt.com/codex/cloud/settings/general). Reviews are triggered when you +- Open a pull request for review +- Mark a draft as ready +- Comment "@codex review". + +If Codex has suggestions, it will comment; otherwise it will react with 👍. + + +Codex can also answer questions or update the PR. Try commenting "@codex address that feedback". + +
+ +### COMMENTED — @copilot-pull-request-reviewer (2026-05-23T21:50:39Z) + +## Pull request overview + +Adds a project-local `tools/lean4/README.md` to improve publication readiness of the Lean 4 artifact by documenting layout, build steps, paper↔theorem mapping, and CI linkage (including a workflow badge). + +**Changes:** +- Added `tools/lean4/README.md` describing the Lean 4 proof artifact, structure, and how to build it locally. +- Added a GitHub Actions badge + CI workflow pointer for the Lean proof gate. +- Added documentation tables for paper-to-Lean mapping and predicate hierarchy. + +## Review threads + +### Thread 1: tools/lean4/README.md:9 (resolved) + +**@chatgpt-codex-connector** (2026-05-23T21:49:27Z): + +**![P2 Badge](https://img.shields.io/badge/P2-yellow?style=flat) Correct the blanket no-`sorry` verification claim** + +Revise this statement because it currently overclaims proof completeness: `tools/lean4/ImaginaryStack/ToyModel.lean` still contains unresolved `sorry` placeholders (e.g., lines 130, 141-142), so not every theorem in `tools/lean4/**` is fully machine-checked. This can mislead reviewers about artifact maturity and publication readiness, especially since the Lean CI job type-checks `Lean4/DbspChainRule.lean` rather than proving all files under `tools/lean4`. + +Useful? React with 👍 / 👎. + +### Thread 2: tools/lean4/README.md:44 (resolved) + +**@copilot-pull-request-reviewer** (2026-05-23T21:50:38Z): + +The “Lean file:line” column doesn’t match the values provided (they reference “Section 4/6” rather than a line range). Either rename the column to something like “Location” or switch the entries to concrete line numbers to keep the mapping unambiguous and greppable. + +### Thread 3: tools/lean4/README.md:103 (resolved) + +**@copilot-pull-request-reviewer** (2026-05-23T21:50:38Z): + +The CI description says the workflow “runs `lake build`”, but the workflow actually runs `lake env lean Lean4/DbspChainRule.lean` (after `lake exe cache get`). Please update this section to reflect the real command(s) so readers don’t cargo-cult the wrong invocation when debugging CI vs local builds. + +### Thread 4: tools/lean4/README.md:139 (resolved) + +**@copilot-pull-request-reviewer** (2026-05-23T21:50:39Z): + +This line includes persona name attribution (“Soraya”) in a current-state README under `tools/`. Repo convention is to use role references outside the explicitly allowed history/research surfaces and roster-mapping sections. Consider changing this to a role-ref (e.g., “the formal-verification expert”) while keeping the link target the same. + +### Thread 5: tools/lean4/README.md:32 (resolved) + +**@copilot-pull-request-reviewer** (2026-05-23T21:50:39Z): + +The build instructions use a pipe-to-shell install (`curl … | sh`), which is an unsafe pattern (executes network content without review) and conflicts with the repo’s supply-chain guidance. Also, it bypasses the project’s canonical three-way-parity bootstrap (`tools/setup/install.sh`), which already installs elan with a pinned commit + SHA256 verification. Recommend switching the setup step to `tools/setup/install.sh` (or, if documenting manual elan install, download-to-file + verify/inspect before running). + +### Thread 6: tools/lean4/README.md:8 (resolved) + +**@copilot-pull-request-reviewer** (2026-05-23T21:50:39Z): + +This README claims “Every theorem here has a machine-checked proof body — no `sorry`, no `admit`”, but `tools/lean4/ImaginaryStack/ToyModel.lean` currently contains multiple `sorry` placeholders. Please narrow the claim (e.g., to `Lean4/DbspChainRule.lean` or to “artifact-grade” modules) or remove it so the README stays truthful. diff --git a/docs/research/shadow-lesson-log-20260522-stale-locks.md b/docs/research/shadow-lesson-log-20260522-stale-locks.md new file mode 100644 index 0000000000..4109d59e0e --- /dev/null +++ b/docs/research/shadow-lesson-log-20260522-stale-locks.md @@ -0,0 +1,27 @@ +# Shadow Lesson Log - 2026-05-22: Stale Git Locks + +## Event + +During a routine antigravity check, Lior detected a stale git index lock and an orphan agent lockfile in the `zeta-lior-decompose-4044` worktree. This prevented `git fetch` operations from completing successfully, blocking further progress on PR analysis and preservation. + +## Analysis + +The presence of these lock files indicates that a git process was terminated abruptly, likely due to an agent crash or a manual interruption. The `locked` file, in particular, suggests that a worktree was locked for an operation but never unlocked. + +This event highlights a vulnerability in our autonomous system. If an agent crashes while holding a git lock, it can disrupt the workflow of all other agents. + +## Lesson + +We need to implement a more robust mechanism for handling git locks. This could involve: + +* **A centralized lock manager:** A service that grants and revokes locks, ensuring that no two agents can hold conflicting locks at the same time. +* **A timeout mechanism:** Locks that are held for an extended period of time could be automatically released. +* **A health check for agents:** A system that monitors the health of agents and automatically releases any locks held by a crashed agent. + +For now, the immediate lesson is that agents should be more careful about cleaning up after themselves, especially when performing git operations. + +## Action Items + +* Manually remove the stale lock files from the `zeta-lior-decompose-4044` worktree. +* Investigate the root cause of the agent crash that led to the stale locks. +* Begin research and design for a more robust git lock management system.