- Remove Float from Core/SilverSightCore.lean (Receipt.pathCost is now Option Nat) - Prove TIC theorems tic_never_decreases and computation_generates_time - Add lakefile.lean, lean-toolchain, and .gitignore for .lake/ - Port Research-Stack Semantics.FixedPoint.lean to formal/CoreFormalism/FixedPoint.lean - Delete thin Q16_16_Spec.lean; update Python/QUBO comments and docs - Create AGENTS.md distilled from Research Stack core bindings - Update REBASE_RULES.md to strip legacy hacks and reference AGENTS.md Build: 2978 jobs, 0 errors (lake build)
11 KiB
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
- Lean is the source of truth. Python and Verilog are extraction targets only.
- 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 newformal/*.leanmodule). - 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, orQ16_16.ofRawInt. - Advancing promotion status in shim space? → STOP.
not_promoteduntil 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.
- No
Floatin Lean compute paths.ofFloatis permitted only at JSON/sensor boundaries and must be immediately bracketed.Floatis forbidden inCore/entirely. - Post-interaction workflow (mandatory after any code/receipt/architecture change):
- Update the nearest scoped
AGENTS.mdfor every touched subtree. - Run the narrow Lean target first, then full
lake buildif Lean files touched. - Commit with an explicit file list; never
git add .. - Run
git status --branch --short --untracked-files=all.
- Update the nearest scoped
- Do Not Sweep: never run
git add .,git checkout -- ., orgit clean -fdx. - Secrets are runtime-only: use environment variables (
OLLAMA_API_KEY,DEEPSEEK_API_KEY, etc.); never commit literal keys. - 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=truein 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.jsonand.roo/mcp.jsonwith current server paths. - Update
.contextstream/config.jsonwith 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 Compilerand 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.leanis the root authority and imports nothing.- The
Receiptis the sole Core/library boundary. Lean stamps; libraries format/store. python/andqubo/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_convergenceandreceipt_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.