diff --git a/docs/RRC_PLACEMENT.md b/docs/RRC_PLACEMENT.md deleted file mode 100644 index cc32a46b..00000000 --- a/docs/RRC_PLACEMENT.md +++ /dev/null @@ -1,161 +0,0 @@ -# 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 |