# REBASE RULES — SilverSight Agent / Rules Manifest

**Purpose:** This file is a rebase seed. When starting a fresh project map, copy only
the files and rules listed here. Do not migrate runtime state, stale audits,
completed assignment boards, or legacy deployment hacks.

**Principle:** *Port the contracts and the rituals, not the state.*

**Status:** Research Stack contained many legacy hacks (Hermes ports, Headroom
proxy endpoints, old benchmark tables, repo-specific paths). Those have been
stripped. The core conceptual bindings — Lean authority, no-Float compute,
receipt boundaries, programming-choice flow, and the post-interaction ritual —
are preserved here and in `AGENTS.md`.

---

## 1. Core Operating Contracts (MUST PORT)

These files are the source of truth for every agent, skill, and editor hook.
They are actively maintained and cross-referenced throughout the stack.

| File | Scope |
|------|-------|
| `AGENTS.md` (this repo) | **SilverSight master operating contract.** Distilled from Research Stack; strips legacy deployment details and adapts rules to the library-method architecture. |
| `0-Core-Formalism/lean/Semantics/AGENTS.md` | Lean/Semantics local contract: blessed Compiler surface, build baselines, quarantine boundaries, proof-tactic lessons, current solidification anchors. **ADAPT** to `formal/AGENTS.md` in SilverSight. |
| `4-Infrastructure/AGENTS.md` | Infrastructure and shim contract: storage stack, hardware-witness boundaries, ENE schema, compute dispatch pattern. **PORT ONLY IF** infrastructure work continues; otherwise drop. |
| `6-Documentation/docs/AGENTS.md` | Strict LLM operating rules: anti-drift evidence standards, `bind` primitive, naming conventions, sigma levels, SI units, deletion criteria, PQC policy. **ADAPT** to `docs/AGENTS.md` if strict doc rules are needed. |
| `5-Applications/text-to-cad/AGENTS.md` | CAD harness contract: generated CAD/URDF source-of-truth, viewer handoff, repo policies. **PORT ONLY IF** CAD work continues. |
| `scripts/qc-flag/AGENTS.md` | Lean QC protocol: 7-check inspection protocol. **ADAPT** to `tests/qc-flag/AGENTS.md` if the protocol is adopted. |
| `shared-data/artifacts/lean_expert_agent/AGENTS.md` | Lean expert agent `/inspect` protocol and output format. **ADAPT** if a formal reviewer agent is wired up. |
| `.github/RRC_OPERATING_CONTRACT.md` | Rainbow Raccoon Compiler gate definition: ACCEPT / HOLD / QUARANTINE. **ADAPT** to SilverSight's receipt gate if RRC work continues. |

### Non-negotiable rules extracted from the contracts

1. **Lean is the source of truth.** Python and Verilog are extraction targets only.
2. **Programming choice flow** — before writing new logic, check this decision tree in order:
   - Admissibility / routing / alignment / gating decision? → **Lean only.**
   - Minting/stamping a top-level receipt or JSON bundle? → **Lean stamps; Python formats/stores only.**
   - Classifying rows / computing alignment scores? → **Lean (`formal/CoreFormalism/` or a new `formal/*.lean` module).**
   - Supplying raw input features (expression text, IDs, weak_axes)? → **Python shim OK,** no admissibility logic, regenerable from source.
   - Float arithmetic in a compute path? → **STOP.** Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt`.
   - Advancing promotion status in shim space? → **STOP.** `not_promoted` until a Lean gate passes.
   - Pure I/O (read/write JSON, subprocess, format output)? → **Python shim OK.** Receipt output is stamped in Lean and stored by Python.
3. **No `Float` in Lean compute paths.** `ofFloat` is permitted only at JSON/sensor boundaries and must be immediately bracketed. `Float` is forbidden in `Core/` entirely.
4. **Post-interaction workflow** (mandatory after any code/receipt/architecture change):
   - Update the nearest scoped `AGENTS.md` for every touched subtree.
   - Run the narrow Lean target first, then full `lake build` if Lean files touched.
   - Commit with an explicit file list; **never** `git add .`.
   - Run `git status --branch --short --untracked-files=all`.
5. **Do Not Sweep:** never run `git add .`, `git checkout -- .`, or `git clean -fdx`.
6. **Secrets are runtime-only:** use environment variables (`OLLAMA_API_KEY`, `DEEPSEEK_API_KEY`, etc.); never commit literal keys.
7. **Legacy recovery is explicit:** use `RECOVER LEGACY INFORMATION: <path/commit/concept>` only. Cross-repo cornfield ref: `backup/distilled-with-vcd-history-2026-05-11`.

---

## 2. Editor / Agent Configs (MUST PORT)

These files inject the contracts into editor/agent runtimes.

| File | Purpose |
|------|---------|
| `.cursorrules` | Cursor: ContextStream `init()`/`context()`/`search()` rules. |
| `.devin/config.json` | Devin: programming-choice reminder hook. |
| `.devin/hooks.json` | Devin: ContextStream hooks. |
| `.devin/hooks/programming-choice-reminder.sh` | Injects programming-choice flow + post-interaction checklist before every user message. |
| `.claude/settings.json` | Claude Code: ContextStream hooks. |
| `.cursor/hooks.json` | Cursor: ContextStream hooks. |
| `.roo/mcp.json` | Roo: MCP server definitions. |
| `.mcp.json` (root) | Minimal MCP config: filesystem, git, fetch, contextstream, lean, remote-lean-proof, sympy, wolfram, aws, github, headroom. |
| `.contextstream/config.json` | ContextStream workspace/project IDs. |
| `.kilo/rules/contextstream.md` | Kilo Code manual ContextStream rules (no hooks available). |
| `.roo/rules/contextstream.md` | Roo Code ContextStream rules. |
| `.windsurf/rules/contextstream.md` | Windsurf ContextStream rules. |

### ContextStream-first workflow (enforced or self-enforced in every editor)

- **First message:** `init(folder_path=...)` → `context(user_message=...)`.
- **Subsequent messages:** `context(user_message=...)` FIRST.
- **Before any file search:** `search(mode="auto")` BEFORE Glob/Grep/Read/Explore/Task/EnterPlanMode.
- **After edits:** `project(action="index")` in editors without auto-indexing.
- **Save transcripts:** `save_exchange=true` in editors without auto-saving.

---

## 3. Skills (MUST PORT)

| Skill | Path | Purpose |
|-------|------|---------|
| `lean-proof` | `.devin/skills/lean-proof/SKILL.md` | Mandatory for all Lean work: proof quality, Q16_16 contract, `#eval` witnesses, promotion gate. |
| `contextstream-workflow` | `.github/skills/contextstream-workflow/SKILL.md` | Persistent memory: plans, tasks, decisions, lessons. |
| `research-stack-workflow` | `.github/skills/research-stack-workflow/SKILL.md` | Token-efficient proof workflow; local inference first on neon. |
| `headroom` | `.opencode/skills/headroom/SKILL.md` | Context compression and cross-agent memory. |
| `cad` | `5-Applications/text-to-cad/skills/cad/SKILL.md` | Script-driven STEP/STL/DXF/GLB generation. |
| `urdf` | `5-Applications/text-to-cad/skills/urdf/SKILL.md` | URDF generation and validation. |
| `rrc-compile` | `.claude/skills/rrc-compile/SKILL.md` | RRC pipeline orchestrator. |
| `rrc-scale-analysis` | `.claude/skills/rrc-scale-analysis/SKILL.md` | RRC pre-flight Q16_16 scale-band analysis. |

---

## 4. MCP Servers (MUST PORT)

From `.mcp.json` / `.roo/mcp.json`:

| Server | Role |
|--------|------|
| `contextstream` | Persistent memory / context / search |
| `filesystem` | Read/write proof artifacts and receipts |
| `git` | History, blame, diff |
| `fetch` | HTTP docs and RFCs |
| `lean` | Lean 4 / Mathlib typecheck bridge |
| `remote-lean-proof` | Hermes / OpenCode / Codex proof backend |
| `sympy` | Symbolic arithmetic verification |
| `wolfram-alpha` | Formula verification (needs `WOLFRAM_APP_ID`) |
| `aws` | AWS API access |
| `github` | PRs, issues, CI |
| `headroom` | Token / context compression |

---

## 5. Conditional Items (PORT ONLY IF DOMAIN REMAINS ACTIVE)

| File | Condition |
|------|-----------|
| `.windsurf/lifeguard.yaml` | Keep only if genetics / GCCL / Mass Number abstraction work continues. Contains safety doctrine for biological-equivalence claims, reverse-collapse, bounded recursion, and claim-state hygiene. |
| `.opencode/agents/*.md` | Keep only if the target sorry/theorem is still open in the new rebase. These are task-specific subagent prompts. |
| `.claude/workflows/ground-disproved-theorems.js` | Keep only if Claude Code still uses this workflow. |

---

## 6. DROP — Do Not Port

| Item | Reason |
|------|--------|
| `.consolidation-manifests/` | Historical SHA256 manifests from 2026-05-04. Not load-bearing. |
| `.headroom/*.db` | Runtime memory databases; regenerate on first use. |
| `.agents/plugins/marketplace.json` | References a dormant `./plugins/substack-connector`. Not load-bearing. |
| `.github/copilot-instructions.md` | Core rules are valid, but the "Current Project State" block is stale (2026-05-28). Port rules separately, not this file as authority. |
| `.windsurf/SORRY_AUDIT.md` | Stale audit (2026-05-28). Root `AGENTS.md` now reports 0 sorries in the active Compiler surface. Archive only. |
| `.windsurf/ASSIGNMENTS.md` | Dated 2026-04-19; all assignments marked COMPLETE and references old paths. Historical residue. |
| Staging manifests (`stack_solidification_staging_manifest_2026-05-09.md`, etc.) | Historical archives; referenced but not authoritative. |
| Cornfield / legacy branches | Do not merge or base work on them. Use only via explicit recovery trigger. |

---

## 7. Minimal Rebase Checklist

Use this when standing up the new project map.

- [ ] Copy all files in **Section 1** (Core Operating Contracts).
- [ ] Copy all files in **Section 2** (Editor / Agent Configs).
- [ ] Copy all files in **Section 3** (Skills).
- [ ] Copy/adapt `.mcp.json` and `.roo/mcp.json` with current server paths.
- [ ] Update `.contextstream/config.json` with new workspace/project IDs if they change.
- [ ] Review **Section 5** conditional items and keep only active-domain rules.
- [ ] Verify **Section 6** dropped items are not carried over.
- [ ] Run `lake build Compiler` and confirm job count matches the new baseline.
- [ ] Update build baseline and commit hash in `0-Core-Formalism/lean/Semantics/AGENTS.md`.

---

## 8. Design Note for the New Map

When designing the new project layout, preserve these boundary rules:

- **Lean owns decisions; Python owns I/O.**
- **`Core/SilverSightCore.lean` is the root authority and imports nothing.**
- **The `Receipt` is the sole Core/library boundary.** Lean stamps; libraries format/store.
- **`python/` and `qubo/` are I/O and optimization shims only.** No admissibility logic in shim space.
- **Research artifacts go outside the git tree** unless promoted as durable receipts.
- **Every new compression path needs two Lean theorems:** `eigensolid_convergence` and `receipt_invertible`.
- **No library imports another library.** Libraries import `Core/` only.

---

*Generated from active Research Stack agent rules and contracts, stripped of legacy hacks.*
*Principle: port contracts and rituals, not state.*
*SilverSight master contract: `AGENTS.md`.*