docs(archive): preserve PR #4772

.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}`;

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`
+
+
+<details> <summary>ℹ️ About Codex in GitHub</summary>
+<br/>
+
+[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".
+
+</details>
+
+### 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):
+
+**<sub><sub>![P2 Badge](https://img.shields.io/badge/P2-yellow?style=flat)</sub></sub>  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.

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.