Archive RRC_PLACEMENT.md

archive/2026-07-02/docs/RRC_PLACEMENT.md

@@ -0,0 +1,161 @@
+# RRC (Rainbow Raccoon Compiler) — Library Placement
+
+## What RRC Actually Is
+
+From `PVGS_DQ_Bridge_fixed.lean` §4:
+
+```lean
+structure RRCEvidence where
+  typeWitness        : ℚ
+  projectionWitness  : ℚ
+  mergeWitness       : ℚ
+  typeAdmissible     : Prop      -- gate 1: type check
+  projectionAdmissible : Prop    -- gate 2: projection check
+  mergeAdmissible    : Prop      -- gate 3: merge check
+
+def kernelEvidence (x m y n : ℕ) : RRCEvidence
+
+theorem goormaghtigh_passes_rrc  -- known solutions pass
+theorem unknown_fails_rrc        -- unknown solutions fail (Goormaghtigh)
+```
+
+RRC is a **receipt compiler** — it takes receipts and compiles them through
+three gates. Each gate is a semantic validation:
+
+| Gate | What it checks | Physical meaning |
+|------|---------------|------------------|
+| **Type** | `|witness| < 1/x` | Is the expression structurally valid? |
+| **Projection** | `|witness| < 1/(xm)` | Does it project cleanly onto the manifold? |
+| **Merge** | `|R1-R2|/(R1+R2) < 10⁻⁶` | Can two receipts coexist without collision? |
+
+## Where It Fits: Its Own Library
+
+RRC is NOT AuditLib. AuditLib checks receipt *format* (well-formedness).
+RRC checks receipt *semantics* (mathematical validity through polynomial gates).
+
+```
+                    SilverSightCore.lean
+                          │
+              ┌───────────┼───────────┐
+              │           │           │
+          LexLib    SearchLib   StructureLib
+              │           │           │
+              └───────────┼───────────┘
+                          │
+                    Receipt produced
+                          │
+              ┌───────────┼───────────┐
+              │           │           │
+          AuditLib    RRCLib      EventLib
+          (format)   (semantics)   (count)
+              │           │           │
+              └───────────┴───────────┘
+                          │
+                   Core.accept / reject
+```
+
+## RRCLib — Rainbow Raccoon Compiler Library
+
+**Type signature:**
+```lean
+-- RRCLib.lean
+import SilverSightCore
+
+-- Compile a receipt through RRC gates
+def RRCLib.compile (r : Receipt) : RRCResult
+
+-- Gate verdicts
+structure RRCResult where
+  typeGate        : GateVerdict
+  projectionGate  : GateVerdict
+  mergeGate       : GateVerdict
+  compiled        : Bool  -- all gates pass
+  deriving Repr
+
+inductive GateVerdict
+  | Pass   -- witness below threshold
+  | Fail   -- witness above threshold
+  | Borderline  -- within 10% of threshold (needs human)
+  deriving DecidableEq, Repr
+```
+
+**What RRCLib does NOT do:**
+- Does NOT produce the initial receipt (that's SearchLib/LexLib)
+- Does NOT count TIC (that's EventLib)
+- Does NOT check receipt format (that's AuditLib)
+- Does NOT compute the Finsler metric (that's MetricLib)
+
+**What RRCLib DOES do:**
+- Takes an existing receipt
+- Evaluates the H-KdF polynomial at the receipt's parameters
+- Checks three gate thresholds
+- Returns Pass/Fail/Borderline for each gate
+- The receipt is **admissible** only if all three gates Pass
+
+## The Key Insight
+
+RRC is a **compiler** because:
+- Input: receipt (source code)
+- Process: three-pass gate evaluation (compilation passes)
+- Output: compiled result with verdicts (executable decision)
+
+The "Rainbow" part: each gate filters a different **color** (aspect) of the receipt:
+- Type = red channel (structural validity)
+- Projection = green channel (manifold fit)
+- Merge = blue channel (collision freedom)
+
+All three must be clear for the receipt to be white (valid).
+
+## RRC as Meta-Library
+
+RRC can also validate receipts ABOUT receipts (meta-recursion):
+
+```lean
+-- Receipt from RRCLib about another receipt
+def RRCLib.metaCompile (r : Receipt) (rrcReceipt : Receipt) : RRCResult
+```
+
+This is how you get the self-indexing property: RRC receipts about RRC receipts,
+forming a hash chain (which is what `pvgs_receipt_hash.py` implements).
+
+## Current Code Location
+
+Your `PVGS_DQ_Bridge_fixed.lean` §4 (`hermitianRRCKernel` through
+`rrc_characterizes_goormaghtigh`) becomes:
+
+```
+SilverSight/
+├── Core/
+│   └── SilverSightCore.lean        ← 200 lines, never changes
+├── Library/
+│   ├── LexLib.lean                 ← your token work
+│   ├── SearchLib.lean              ← your chaos game work
+│   ├── MetricLib.lean              ← your Finsler work
+│   ├── QUBOLib.lean                ← your QUBO/QAOA work
+│   ├── StructureLib.lean           ← your ChiralitySpace work
+│   ├── PVGSLib.lean                ← your PVGS bridge work
+│   ├── EventLib.lean               ← your TIC counting work
+│   ├── AuditLib.lean               ← format validation
+│   └── RRCLib.lean                 ← §4 of PVGS_DQ_Bridge_fixed.lean
+│       ├── RRCGates.lean           -- gate definitions
+│       ├── RRCKernel.lean          -- hermitianRRCKernel
+│       ├── RRCEvidence.lean        -- RRCEvidence structure
+│   └── RRCLib/                     -- NEW: RRC as standalone library
+│       ├── RRCReceipt.lean         -- receipt validation
+│       ├── RRCMeta.lean            -- meta-receipt validation
+│       └── RRCHashChain.lean       -- from pvgs_receipt_hash.py
+└── Orchestrator/
+    └── SilverSight.lean            -- composes everything
+```
+
+## Summary
+
+| Question | Answer |
+|----------|--------|
+| Is RRC AuditLib? | No — AuditLib checks format, RRC checks semantics |
+| Is RRC SearchLib? | No — SearchLib finds basins, RRC validates receipts |
+| Is RRC its own library? | **Yes** — RRCLib, importing only Core |
+| What does RRC compile? | Receipts through 3 polynomial gates |
+| Why "Rainbow"? | 3 gates = 3 color channels = white if all pass |
+| Why "Raccoon"? | Because raccoons wash everything before accepting it |
+| Why "Compiler"? | Source receipt → gate passes → compiled verdict |