# AGENTS.md — SilverSight Operating Contract **Principle:** *Port the contracts and the rituals, not the state.* This file distills the surviving rules from Research Stack and rebases them onto SilverSight's library-method architecture. Legacy deployment details, stale benchmark tables, and repo-specific paths have been stripped. The conceptual bindings — Lean authority, no-Float compute, receipt boundaries, and the post-interaction ritual — remain in force. --- ## 1. Project Architecture SilverSight is organized as a minimal invariant core plus independent libraries. ``` Core/ SilverSightCore.lean ← no imports, no Float, no library code SilverSight/FixedPoint.lean ← canonical Q16_16 / Q0_16 (core contract) formal/ CoreFormalism/ ← Hachimoji, Chentsov, Sidon, braid foundations PVGS_DQ_Bridge/ ← quantum bridge UniversalEncoding/ ← math address space BindingSite/ ← biological binding sketches SilverSight/ ← RRC decision surface + AVM ISA (namespace roots) RRCLib/ ← user-facing symlinks to formal/SilverSight/ python/ ← I/O, feature extraction, orchestration qubo/ ← optimization libraries tests/ ← verification fixtures docs/ ← architecture and placement docs ``` **Living map:** `docs/PROJECT_MAP.md` / `docs/PROJECT_MAP.json` — regenerate with `python3 docs/generate_project_map.py` after adding, moving, or removing files. ### Library method - **Core defines the contract.** Libraries implement it. - `Core/SilverSightCore.lean` imports nothing and depends on nothing. - Every library may import `Core/` but may **not** import another library. - The `Receipt` is the only interface between Core and libraries. --- ## 2. The No-Float Law **No `Float` in Lean compute paths.** This is non-negotiable. - Use `Q16_16.ofNat`, `Q16_16.ofRatio`, or `Q16_16.ofRawInt` for all core arithmetic. - `ofFloat` is permitted **only** at external boundaries (JSON parsing, sensor input) and must be immediately bracketed/converted. - `Float` is forbidden in `Core/` entirely. `Receipt.pathCost` is an `Option Nat` (raw fixed-point integer), not `Option Float`. - The canonical fixed-point implementation is `Core/SilverSight/FixedPoint.lean`, ported from Research Stack `Semantics.FixedPoint.lean` with boundary conversions removed from compute paths. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. --- ## 3. Programming Choice Flow Before writing or placing any new logic, run through this decision tree in order. Stop at the first rule that applies. ``` New logic needed? │ ├── Does it make an admissibility, routing, alignment, or gating decision? │ └── YES → Write it in Lean. No Python equivalent allowed. │ File: formal/CoreFormalism/*.lean or a new formal/*.lean module. │ ├── Does it mint, stamp, or emit a top-level receipt or JSON bundle? │ └── YES → It belongs in Core receipt validators or the designated emitter. │ Python may format/store, but Lean stamps the decision. │ ├── Does it classify rows, run an alignment gate, or compute scores? │ └── YES → Lean. Python may call it via #eval / lake exe but may not │ replicate the logic. │ ├── Does it supply raw input features (expression text, route_hint, domain_type, │ equation_id hashing, weak_axes count)? │ └── YES → Python shim is acceptable. The shim must: │ (a) produce only a raw data structure │ (b) carry no admissibility logic │ (c) be regenerable from source │ (d) live in python/ or qubo/ with a TODO(lean-port) if the logic │ could eventually move to Lean │ ├── Does it use floating-point arithmetic in a compute path? │ └── YES → STOP. Use Q16_16.ofNat / Q16_16.ofRatio / Q16_16.ofRawInt. │ ├── Does it advance promotion status (e.g. set promotion = "promoted")? │ └── YES → STOP. Promotion is always not_promoted until a Lean gate │ explicitly passes. Never advance it in shim space or by hand. │ └── Is it pure I/O (read JSON, write JSONL, call subprocess, format output)? └── YES → Python shim is fine. Keep it in python/ or qubo/. ``` **Summary:** Lean owns all decisions. Python owns all I/O. --- ## 4. Receipt Contract The `Receipt` is the compressed interface record. It is not metadata around a result; it **is** the result. ```lean structure Receipt where receiptID : String expression : String finalState : HachimojiState ticCount : Nat fuelUsed : Nat pathCost : Option Nat -- raw integer cost; never Float libraryRefs : List String verified : Bool ``` - Libraries produce receipts. The core consumes them. - A receipt proves only the gate it actually checks. - Receipt validation lives in `Core/SilverSightCore.lean`. --- ## 5. AVM and TIC Axiom The Abstract Virtual Machine (AVM) is a stack machine defined in Core. - `δ : AVMState × Instruction → AVMState` is the sole transition function. - **TIC axiom:** TIC is derived from events, never the driver. - `T_{n+1} = T_n + E(S_n)` where `E ≥ 0` - `δ` never decreases TIC. - Meaningful computation (`finalState ≠ Ζ`) implies `ticCount > 0`. --- ## 6. Verification Expectations See `docs/TESTING.md` for the full testing contract. Quick checks: - For Lean changes, run the narrow target first, then `lake build` when feasible. Record the build baseline in `docs/build_logs/YYYY-MM-DD_session_build_baseline.md`. - After adding, moving, or removing files, regenerate `docs/PROJECT_MAP.md` and `docs/PROJECT_MAP.json` with `python3 docs/generate_project_map.py`. - For Python shims, run `python3 -m py_compile` on touched files and add a matching `tests/test_*.py` unit test. - Run `python3 .github/scripts/glossary_lint.py` after adding new domain terms to documentation. - For JSON receipts, run `python3 -m json.tool`. - Before committing, run `git diff --cached --check` and scan touched files for secrets. --- ## 7. Post-Interaction Workflow (mandatory) After any code, Lean, shim, receipt, or architecture change: 1. **Update the nearest scoped AGENTS.md.** - Root or multi-subtree changes → this file. - `Core/` changes → `Core/AGENTS.md` if one exists, otherwise this file. - `formal/` changes → `formal/AGENTS.md` if one exists, otherwise this file. 2. **Regenerate the project map if files were added, moved, or removed.** ```bash python3 docs/generate_project_map.py ``` 3. **Verify the build.** - Lean: `lake build` from the appropriate `lakefile.lean` root. - Python: `python3 -m py_compile` on touched files. 3. **Commit.** - Stage only explicitly touched files. **Never `git add .`.** - Commit format: ``` (): Build: jobs, 0 errors (lake build) ``` - Types: `feat`, `fix`, `chore`, `docs`, `refactor`. - Scopes: `core`, `formal`, `python`, `qubo`, `docs`, `infra`. 4. **Check tree cleanliness.** ```bash git status --branch --short --untracked-files=all ``` Untracked files that are not generated artifacts must be staged or noted as intentionally dirty. --- ## 8. Do Not Sweep Never run broad cleanup commands: ```bash git add . git checkout -- . git clean -fdx ``` Use explicit file lists. Generated artifacts and research scratch should stay out of Git unless they are themselves the evidence under review. --- ## 9. Git Remote Hygiene - The active branch may not have an upstream. Inspect with `git rev-parse --abbrev-ref --symbolic-full-name @{u}` before assuming push state. - Prefer the `github` remote and verify the remote head after push: ```bash git fetch github git rev-list --left-right --count FETCH_HEAD...HEAD git push -u github git ls-remote --heads github ``` --- ## 10. Secrets Secrets are runtime-only. Use environment variables (`OLLAMA_API_KEY`, `DEEPSEEK_API_KEY`, etc.). Never paste, print, or commit literal provider keys. --- ## 11. Legacy Recovery Trigger The phrase **`RECOVER LEGACY INFORMATION`** is the explicit retrieval trigger for archived or quarantined concepts. Accepted forms: ```text RECOVER LEGACY INFORMATION: Recover Legacy Information: recover from cornfield: ``` Rules: - Inspect the requested legacy source with read-only commands first. - Recover only the named file, concept, commit slice, or receipt. - Modernize the recovered material onto the current clean branch. - Never merge, reset to, or base new work on a legacy branch unless explicitly asked. - Preserve the legacy branch as retrievable archive state. Current Research Stack cornfield ref (for cross-repo lookup only): `backup/distilled-with-vcd-history-2026-05-11`. --- ## 12. Glossary - **Hachimoji state** — one of Φ, Λ, Ρ, Κ, Ω, Σ, Π, Ζ. The 8-state output alphabet of the core classifier. - **Receipt** — the machine-readable attestation record that crosses the Core/library boundary. - **AVM** — Abstract Virtual Machine. The stack-machine semantics defined in `Core/SilverSightCore.lean`. - **TIC** — Temporal Index of Computation. A monotone event counter derived from state transitions. - **Q16_16** — Canonical 32-bit fixed-point type (`Core/SilverSight/FixedPoint.lean`). - **Library method** — Core defines contracts; libraries implement them; no library imports another library. - **Sidon label** — an address from a set with unique pairwise sums. Powers of 2 are canonical for 8 strands. - **BraidStorm** — the 8-strand braid topology used in eigensolid compression. - **eigensolid** — converged stable state of a braid crossing loop; detected when `crossStep(s) = s`. - **promotion** — status advance from `not_promoted` to `promoted` only after a Lean gate passes. --- ## 13. Citation File Format (CFF) Standards `CITATION.cff` must remain valid CFF 1.2.0 and be checked after any edit. - Run `python3 -c "import yaml; yaml.safe_load(open('CITATION.cff'))"` to verify YAML syntax. - Include all required fields: `cff-version`, `message`, `title`, `authors`, `type`. - Use `repository-code` and `url` for the project; add `date-released` and `license` when known. - For references: - Prefer DOI or arXiv ID. Use `url` only when no persistent identifier exists. - Use `type: unpublished` for preprints or works without a confirmed venue; do not invent journal names or placeholder identifiers. - For non-academic sources (e.g. Reddit posts, blog posts, forum threads), use `type: generic` or `type: misc` with a `url` and `date-accessed` note. - Avoid `et al.` as an author entry when a full author list is available; use it only as a last resort for long author lists. - When porting from Research Stack, add Research Stack as a `software` reference, not as a co-author. --- ## 14. SilverSight-Specific Boundaries - `Core/SilverSightCore.lean` is the root authority. It contains no sorries in the active surface. - `Core/SilverSight/FixedPoint.lean` is the canonical Q16_16 / Q0_16 source of truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. - `Core/SilverSight/FixedPoint.lean` is the canonical `Q16_16`/`Q0_16` source of truth. `formal/CoreFormalism/FixedPoint.lean` is a compatibility shim. - `Core/SilverSight/Semantics/` is the YaFF-inspired schema/layout/wireformat core. It now contains `Schema`, `Layout`, `WireFormat`, `View`, `LayoutBridge`, and `CanalLayout`. These modules build under `lake build SilverSightCore` (2987 jobs, 0 errors) and import only Mathlib. - `formal/CoreFormalism/SidonSets.lean` is ported from Research Stack and builds under `lake build CoreFormalism.SidonSets` (2601 jobs, 0 errors). The chaos-game appendix was removed because it did not build; the core Singer theorem, Lindström bound, and interval-Sidon infrastructure are intact. - `formal/CoreFormalism/SieveLemmas.lean` and `formal/CoreFormalism/InteractionGraphSidon.lean` are ported from Research Stack and build under `lake build SilverSightFormal` (3132 jobs, 0 errors). - `formal/CoreFormalism/BraidEigensolid.lean` and `formal/CoreFormalism/BraidSpherionBridge.lean` are ported from Research Stack with namespace `SilverSight.BraidEigensolid` / `SilverSight.BraidSpherionBridge`. Supporting modules (Tactics, Q16_16Numerics, DynamicCanal, Bind, BraidBracket, BraidStrand, BraidCross, BraidField) were added to `lakefile.lean` roots. - `formal/SilverSight/` is the RRC decision surface and concrete AVM ISA. It builds under `lake build SilverSightRRC` (3006 jobs, 0 errors) and imports only `Core/` + Mathlib. User-facing symlinks live in `formal/RRCLib/`. - New RRC gates ported from Research Stack: - `formal/SilverSight/RRC/ReceiptDensity.lean` — Q16_16 receipt-density scoring - `formal/SilverSight/RRC/PolyFactorIdentity.lean` — divisor-sum signature gate - `formal/SilverSight/RRC/EntropyCandidates.lean` — 10 certifiable braid-state fixtures adapted to `CoreFormalism.BraidEigensolid` types - `formal/SilverSight/AVMIsa/Emit.lean` is the sole top-level JSON output boundary for RRC receipts. - `exe/RrcEmitFixture.lean` is the `rrc-emit-fixture` executable that emits the AVM-stamped fixture corpus JSON. - `exe/Q16_16Roundtrip.lean` is the `q16-roundtrip` executable. It links `c/q16_canonical.c` via Lake `extern_lib` and compares Lean `Core/SilverSight/FixedPoint.Q16_16` against the C implementation on raw-bit round-trip, addition, and subtraction. - `c/q16_canonical.c` is the canonical C implementation of Q16_16 conversion, addition, subtraction, multiplication, and division (banker's rounding, saturating arithmetic). - `python/q16_canonical.py` is the canonical Python Q16_16 shim. - `tests/test_q16_roundtrip.py` is the Python ↔ C roundtrip test harness (21 tests, all green). - `python/pist_matrix_builder.py` and `python/validate_rrc_predictions.py` are I/O-only raw-feature shims. They contain no admissibility logic and no Float arithmetic. - `python/hachimoji_citation.py` — Equation → Hachimoji state classifier → arXiv citation retriever. Mirrors `formal/CoreFormalism/HachimojiCodec.lean` exactly. Uses hybrid_search SQL function for trigram+pgvector RRF retrieval. - Build baselines and session summaries are recorded in `docs/build_logs/YYYY-MM-DD_session_build_baseline.md` (see `docs/build_logs/2026-06-21_session_build_baseline.md`). - The `python/` and `qubo/` directories are I/O and optimization shims only; they may not contain admissibility logic. - `docs/GLOSSARY.md` is the authoritative term dictionary. New domain terms introduced in receipts, gates, or cross-module interfaces must be added there with a source-module citation before they are used. - Research artifacts and scratch output should live outside the git tree unless promoted as durable receipts. - RRC status is tracked in `docs/RRC_REFACTOR_READINESS.md`.