Merge tabula-rasa into main

.beads/.gitignore

@@ -0,0 +1,44 @@
+# SQLite databases
+*.db
+*.db?*
+*.db-journal
+*.db-wal
+*.db-shm
+
+# Daemon runtime files
+daemon.lock
+daemon.log
+daemon.pid
+bd.sock
+sync-state.json
+last-touched
+
+# Local version tracking (prevents upgrade notification spam after git ops)
+.local_version
+
+# Legacy database files
+db.sqlite
+bd.db
+
+# Worktree redirect file (contains relative path to main repo's .beads/)
+# Must not be committed as paths would be wrong in other clones
+redirect
+
+# Merge artifacts (temporary files from 3-way merge)
+beads.base.jsonl
+beads.base.meta.json
+beads.left.jsonl
+beads.left.meta.json
+beads.right.jsonl
+beads.right.meta.json
+
+# Sync state (local-only, per-machine)
+# These files are machine-specific and should not be shared across clones
+.sync.lock
+sync_base.jsonl
+
+# NOTE: Do NOT add negation patterns (e.g., !issues.jsonl) here.
+# They would override fork protection in .git/info/exclude, allowing
+# contributors to accidentally commit upstream issue databases.
+# The JSONL files (issues.jsonl, interactions.jsonl) and config files
+# are tracked by git by default since no pattern above ignores them.

.beads/README.md

@@ -0,0 +1,81 @@
+# Beads - AI-Native Issue Tracking
+
+Welcome to Beads! This repository uses **Beads** for issue tracking - a modern, AI-native tool designed to live directly in your codebase alongside your code.
+
+## What is Beads?
+
+Beads is issue tracking that lives in your repo, making it perfect for AI coding agents and developers who want their issues close to their code. No web UI required - everything works through the CLI and integrates seamlessly with git.
+
+**Learn more:** [github.com/steveyegge/beads](https://github.com/steveyegge/beads)
+
+## Quick Start
+
+### Essential Commands
+
+```bash
+# Create new issues
+bd create "Add user authentication"
+
+# View all issues
+bd list
+
+# View issue details
+bd show <issue-id>
+
+# Update issue status
+bd update <issue-id> --status in_progress
+bd update <issue-id> --status done
+
+# Sync with git remote
+bd sync
+```
+
+### Working with Issues
+
+Issues in Beads are:
+- **Git-native**: Stored in `.beads/issues.jsonl` and synced like code
+- **AI-friendly**: CLI-first design works perfectly with AI coding agents
+- **Branch-aware**: Issues can follow your branch workflow
+- **Always in sync**: Auto-syncs with your commits
+
+## Why Beads?
+
+✨ **AI-Native Design**
+- Built specifically for AI-assisted development workflows
+- CLI-first interface works seamlessly with AI coding agents
+- No context switching to web UIs
+
+🚀 **Developer Focused**
+- Issues live in your repo, right next to your code
+- Works offline, syncs when you push
+- Fast, lightweight, and stays out of your way
+
+🔧 **Git Integration**
+- Automatic sync with git commits
+- Branch-aware issue tracking
+- Intelligent JSONL merge resolution
+
+## Get Started with Beads
+
+Try Beads in your own projects:
+
+```bash
+# Install Beads
+curl -sSL https://raw.githubusercontent.com/steveyegge/beads/main/scripts/install.sh | bash
+
+# Initialize in your repo
+bd init
+
+# Create your first issue
+bd create "Try out Beads"
+```
+
+## Learn More
+
+- **Documentation**: [github.com/steveyegge/beads/docs](https://github.com/steveyegge/beads/tree/main/docs)
+- **Quick Start Guide**: Run `bd quickstart`
+- **Examples**: [github.com/steveyegge/beads/examples](https://github.com/steveyegge/beads/tree/main/examples)
+
+---
+
+*Beads: Issue tracking that moves at the speed of thought* ⚡

.beads/config.yaml

@@ -0,0 +1,62 @@
+# Beads Configuration File
+# This file configures default behavior for all bd commands in this repository
+# All settings can also be set via environment variables (BD_* prefix)
+# or overridden with command-line flags
+
+# Issue prefix for this repository (used by bd init)
+# If not set, bd init will auto-detect from directory name
+# Example: issue-prefix: "myproject" creates issues like "myproject-1", "myproject-2", etc.
+# issue-prefix: ""
+
+# Use no-db mode: load from JSONL, no SQLite, write back after each command
+# When true, bd will use .beads/issues.jsonl as the source of truth
+# instead of SQLite database
+# no-db: false
+
+# Disable daemon for RPC communication (forces direct database access)
+# no-daemon: false
+
+# Disable auto-flush of database to JSONL after mutations
+# no-auto-flush: false
+
+# Disable auto-import from JSONL when it's newer than database
+# no-auto-import: false
+
+# Enable JSON output by default
+# json: false
+
+# Default actor for audit trails (overridden by BD_ACTOR or --actor)
+# actor: ""
+
+# Path to database (overridden by BEADS_DB or --db)
+# db: ""
+
+# Auto-start daemon if not running (can also use BEADS_AUTO_START_DAEMON)
+# auto-start-daemon: true
+
+# Debounce interval for auto-flush (can also use BEADS_FLUSH_DEBOUNCE)
+# flush-debounce: "5s"
+
+# Git branch for beads commits (bd sync will commit to this branch)
+# IMPORTANT: Set this for team projects so all clones use the same sync branch.
+# This setting persists across clones (unlike database config which is gitignored).
+# Can also use BEADS_SYNC_BRANCH env var for local override.
+# If not set, bd sync will require you to run 'bd config set sync.branch <branch>'.
+sync-branch: "beads-sync"
+
+# Multi-repo configuration (experimental - bd-307)
+# Allows hydrating from multiple repositories and routing writes to the correct JSONL
+# repos:
+#   primary: "."  # Primary repo (where this database lives)
+#   additional:   # Additional repos to hydrate from (read-only)
+#     - ~/beads-planning  # Personal planning repo
+#     - ~/work-planning   # Work planning repo
+
+# Integration settings (access with 'bd config get/set')
+# These are stored in the database, not in this file:
+# - jira.url
+# - jira.project
+# - linear.url
+# - linear.api-key
+# - github.org
+# - github.repo

.beads/issues.jsonl

@@ -0,0 +1,3 @@
+{"id":"nfp-g0j","title":"Refactor HeadBounds reduction helpers","description":"Deduplicate chunked reduction task helpers in Nfp/Sound/Induction/HeadBounds.lean to reduce proof churn while preserving behavior.","status":"closed","priority":2,"issue_type":"task","owner":"robin.gieseke@me.com","created_at":"2026-01-12T16:21:11.583135+01:00","created_by":"TheDarkchip","updated_at":"2026-01-12T16:22:20.621327+01:00","closed_at":"2026-01-12T16:22:20.621327+01:00","close_reason":"Completed"}
+{"id":"nfp-g78","title":"Refactor CoreSound lemmas for stability","description":"Refactor Nfp/Sound/Induction/CoreSound.lean to reduce proof churn and improve maintainability; keep proofs explicit and stable.","status":"closed","priority":2,"issue_type":"task","owner":"robin.gieseke@me.com","created_at":"2026-01-12T16:12:25.347409+01:00","created_by":"TheDarkchip","updated_at":"2026-01-12T16:16:04.322186+01:00","closed_at":"2026-01-12T16:16:04.322186+01:00","close_reason":"Completed","labels":["in_progress"]}
+{"id":"nfp-snh","title":"Refactor MatrixNorm interval bounds proofs","description":"Refactor Nfp/Sound/Bounds/MatrixNorm/Interval.lean to reduce proof churn and simplify interval bound lemmas.","status":"closed","priority":2,"issue_type":"task","owner":"robin.gieseke@me.com","created_at":"2026-01-12T15:54:50.752468+01:00","created_by":"TheDarkchip","updated_at":"2026-01-12T16:01:12.070535+01:00","closed_at":"2026-01-12T16:01:12.070535+01:00","close_reason":"Closed","comments":[{"id":1,"issue_id":"nfp-snh","author":"TheDarkchip","text":"Refactored foldl_pair helper for pair foldl projections in MatrixNorm interval bounds; adjusted proofs to use Prod.fst/Prod.snd. Fixed CoreSound cdot lint warnings encountered during build.","created_at":"2026-01-12T15:01:08Z"}]}

.beads/metadata.json

@@ -0,0 +1,4 @@
+{
+  "database": "beads.db",
+  "jsonl_export": "issues.jsonl"
+}

.gitattributes

@@ -0,0 +1,3 @@
+
+# Use bd merge for beads JSONL files
+.beads/issues.jsonl merge=beads

.github/workflows/ci.yml

@@ -33,33 +33,3 @@ jobs:
             echo "Quiet build failed; retrying verbose..."
             lake build nfp -v --no-ansi --wfail
           }
-
-      - name: SOUND cache regression test (tiny fixture)
-        run: |
-          set -euo pipefail
-          lake exe nfp sound_cache_check --scalePow10 9 --maxTokens 0 tests/fixtures/tiny_sound_model.nfpt
-
-      - name: Python setup
-        uses: actions/setup-python@v5
-        with:
-          python-version: "3.11"
-
-      - name: Cache HF model files
-        uses: actions/cache@v4
-        with:
-          path: |
-            ~/.cache/huggingface
-            ~/.cache/torch
-          key: ${{ runner.os }}-hf-tiny-gpt2-v1
-
-      - name: Install PyTorch + Transformers (CPU)
-        run: |
-          set -euo pipefail
-          python -m pip install --upgrade pip
-          python -m pip install --index-url https://download.pytorch.org/whl/cpu torch
-          python -m pip install transformers numpy
-
-      - name: Sanity check (Lean vs PyTorch forward step)
-        run: |
-          set -euo pipefail
-          python scripts/ci_sanity_forward_step.py --model sshleifer/tiny-gpt2 --seqLen 8 --layer 0 --pos 0 --take 16

.gitignore

@@ -1,13 +1,9 @@
 /.lake
-models
-*.nfpt
-!tests/fixtures/*.nfpt
 .DS_Store
 logs/
 sound_cache/
 lean-reference-manual/
 inductionhead_papers/
 nfp.zip
 reports/
-tests/fixtures/tiny_sound_binary.nfpt
 nfp_agent_book/