mirror of
https://github.com/allaunthefox/SilverSight.git
synced 2026-07-31 01:25:21 +00:00
6d2136c328
Some checks failed
Replaced 3 monolithic lean_lib (SilverSightCore, SilverSightFormal, SilverSightRRC) with 14 focused modules: Layer 0: SilverSightCore (foundation) Layer 1: SilverSightNumerics (Q16_16, fixed-point) Layer 2: SilverSightCanal (dynamic canal, Bind) Layer 3a: SilverSightBraid (braid theory) Layer 3b: SilverSightSidon (Sidon sets, CRT, sieve) Layer 3c: SilverSightHachimoji (DNA encoding, N=8 proof) Layer 4: SilverSightPIST (spectral classification) Layer 5: SilverSightAVM (ISA) Layer 6: SilverSightRRC (receipt pipeline) Layer 7: SilverSightBindingSite (binding site codec) Layer 8: SilverSightFeasible (QUBO relaxation) Standalone: SilverSightGeometry, SilverSightMisc Each module is independently buildable with clear dependency ordering.
184 lines
6.5 KiB
Markdown
184 lines
6.5 KiB
Markdown
# SilverSight Module Map
|
|
|
|
**Date:** 2026-07-08
|
|
**Status:** Extraction complete — 14 standalone lake targets replacing 3 monolithic ones
|
|
|
|
---
|
|
|
|
## Architecture
|
|
|
|
```
|
|
Layer 0 SilverSightCore .............. Core foundation (Semantics schema, layout, wire format)
|
|
Layer 1 SilverSightNumerics .......... Q16_16 fixed-point, tactics, prime LUT
|
|
Layer 2 SilverSightCanal ............. Dynamic canal, Bind infrastructure
|
|
Layer 3a SilverSightBraid ............. Braid theory (strand → cross → field → eigensolid)
|
|
Layer 3b SilverSightSidon ............. Sidon sets, CRT, sieve lemmas, E8
|
|
Layer 3c SilverSightHachimoji ......... Hachimoji DNA encoding (N=8 proof, phi pipeline)
|
|
Layer 4 SilverSightPIST .............. PIST spectral classification (matrix → spectral → classify)
|
|
Layer 5 SilverSightAVM ............... AVM instruction set architecture (types → safety → emit)
|
|
Layer 6 SilverSightRRC ............... RRC receipt pipeline (emit, density, Q16_16 manifold)
|
|
Layer 7 SilverSightBindingSite ....... Binding site codec (types → hachimoji → entropy → codec)
|
|
Layer 8 SilverSightFeasible .......... QUBO relaxation, feasible set theorems
|
|
SilverSightGeometry .......... Complex projective space, Hopf fibration, Chentsov
|
|
SilverSightMisc .............. Standalone modules (Collatz, GoldenSpiral, AngrySphinx, etc.)
|
|
```
|
|
|
|
## Dependency Graph
|
|
|
|
```
|
|
SilverSightCore (Layer 0)
|
|
└─► SilverSightNumerics (Layer 1)
|
|
├─► SilverSightCanal (Layer 2)
|
|
│ ├─► SilverSightBraid (Layer 3a)
|
|
│ │ └─► [standalone]
|
|
│ └─► [standalone]
|
|
├─► SilverSightSidon (Layer 3b) ──► [standalone, Mathlib only]
|
|
├─► SilverSightHachimoji (Layer 3c) ──► [depends on Core + FixedPoint]
|
|
├─► SilverSightPIST (Layer 4) ──► [depends on Numerics]
|
|
├─► SilverSightAVM (Layer 5) ──► [self-contained ISA]
|
|
├─► SilverSightRRC (Layer 6) ──► [depends on Hachimoji + PIST]
|
|
├─► SilverSightBindingSite (Layer 7) ──► [depends on Hachimoji]
|
|
├─► SilverSightFeasible (Layer 8) ──► [standalone]
|
|
├─► SilverSightGeometry ──► [standalone, Mathlib only]
|
|
└─► SilverSightMisc ──► [standalone, mixed deps]
|
|
```
|
|
|
|
## Module Details
|
|
|
|
### SilverSightCore (Layer 0)
|
|
**Files:** 7 | **srcDir:** `Core/`
|
|
- SilverSightCore.lean
|
|
- SilverSight.FixedPoint.lean
|
|
- SilverSight.Semantics.Schema.lean
|
|
- SilverSight.Semantics.Layout.lean
|
|
- SilverSight.Semantics.WireFormat.lean
|
|
- SilverSight.Semantics.View.lean
|
|
- SilverSight.Semantics.LayoutBridge.lean
|
|
- SilverSight.Semantics.CanalLayout.lean
|
|
|
|
### SilverSightNumerics (Layer 1)
|
|
**Files:** 5 | **srcDir:** `formal/`
|
|
- CoreFormalism.FixedPoint
|
|
- CoreFormalism.Tactics
|
|
- CoreFormalism.Q16_16Numerics
|
|
- SilverSight.PrimeLut
|
|
- SilverSight.FixedPointBridge
|
|
|
|
### SilverSightCanal (Layer 2)
|
|
**Files:** 2 | **srcDir:** `formal/`
|
|
- CoreFormalism.DynamicCanal
|
|
- CoreFormalism.Bind
|
|
|
|
### SilverSightBraid (Layer 3a)
|
|
**Files:** 8 | **srcDir:** `formal/`
|
|
- CoreFormalism.BraidBracket
|
|
- CoreFormalism.BraidStrand
|
|
- CoreFormalism.BraidCross
|
|
- CoreFormalism.BraidField
|
|
- CoreFormalism.BraidStateN
|
|
- CoreFormalism.BraidEigensolid
|
|
- CoreFormalism.BraidSpherionBridge
|
|
- CoreFormalism.ContractedCrossStep
|
|
|
|
### SilverSightSidon (Layer 3b)
|
|
**Files:** 9 | **srcDir:** `formal/`
|
|
- CoreFormalism.SidonSets
|
|
- CoreFormalism.SieveLemmas
|
|
- CoreFormalism.InteractionGraphSidon
|
|
- CoreFormalism.CRTSidon
|
|
- CoreFormalism.CRTSidonN
|
|
- CoreFormalism.E8Sidon
|
|
- CoreFormalism.EisensteinSeries
|
|
- CoreFormalism.GoormaghtighEnumeration
|
|
- CoreFormalism.StrandCapacityBound
|
|
|
|
### SilverSightHachimoji (Layer 3c)
|
|
**Files:** 11 | **srcDir:** `formal/`
|
|
- CoreFormalism.HachimojiBase
|
|
- CoreFormalism.HachimojiCodec
|
|
- CoreFormalism.HachimojiLUT
|
|
- CoreFormalism.HachimojiBridging
|
|
- CoreFormalism.HachimojiManifoldAxiom
|
|
- SilverSight.HachimojiN8
|
|
- SilverSight.HachimojiN8Bridge
|
|
- SilverSight.HachimojiCharClass
|
|
- SilverSight.PhiDNALayout
|
|
- SilverSight.PhiConsistency
|
|
- SilverSight.PhiPipelineReceipt
|
|
|
|
### SilverSightPIST (Layer 4)
|
|
**Files:** 21 | **srcDir:** `formal/`
|
|
- SilverSight.PIST.Spectral, SpectralN, MatrixN, CharPoly
|
|
- SilverSight.PIST.FisherRigidity, FisherRigidityN
|
|
- SilverSight.PIST.Classify, ClassifyN
|
|
- SilverSight.PIST.Matrices250, UnifiedCovariant, CartanConnection
|
|
- SilverSight.PIST.YangBaxter, SidonMirrorNotch, Tdoku16D
|
|
- SilverSight.PIST.CrossDomainSynthesis, MultiSurfacePacker, ManifoldShortcut
|
|
- SilverSight.PIST.SidonAdapter, WeightCandidateGen, UnitDistCandidateGen, CMYKColoringCore
|
|
|
|
### SilverSightAVM (Layer 5)
|
|
**Files:** 9 | **srcDir:** `formal/`
|
|
- SilverSight.AVMIsa.Types, Value, Instr, State, Step
|
|
- SilverSight.AVMIsa.TypeCheck, TypeSafety, Run, Emit
|
|
|
|
### SilverSightRRC (Layer 6)
|
|
**Files:** 8 | **srcDir:** `formal/`
|
|
- SilverSight.RRCLogogramProjection
|
|
- SilverSight.ReceiptCore
|
|
- SilverSight.RRC.Emit, ReceiptDensity, PolyFactorIdentity, EntropyCandidates, Q16_16Manifold
|
|
- RRCLib.RRCEmit
|
|
|
|
### SilverSightBindingSite (Layer 7)
|
|
**Files:** 4 | **srcDir:** `formal/`
|
|
- BindingSite.BindingSiteTypes
|
|
- BindingSite.BindingSiteHachimoji
|
|
- BindingSite.BindingSiteEntropy
|
|
- BindingSite.BindingSiteCodec
|
|
|
|
### SilverSightFeasible (Layer 8)
|
|
**Files:** 2 | **srcDir:** `formal/`
|
|
- SilverSight.FeasibleSet.Theorem
|
|
- SilverSight.FeasibleSet.QUBORelaxation
|
|
|
|
### SilverSightGeometry
|
|
**Files:** 4 | **srcDir:** `formal/`
|
|
- CoreFormalism.ComplexProjectiveSpace
|
|
- CoreFormalism.ChentsovFinite
|
|
- CoreFormalism.HopfFibration
|
|
- CoreFormalism.AutoProof
|
|
|
|
### SilverSightMisc
|
|
**Files:** 19 | **srcDir:** `formal/`
|
|
- SilverSight.AngrySphinx, BlockCoprimeDensity, CollatzBraid, GoldenSpiral, GCCL
|
|
- SilverSight.WireFormat, ProductSchema, ProductWireFormat, Receipt
|
|
- SilverSight.AdjugateMatrix, ChiralClockModel, ColdReviewer, HCMR, CacheSieve
|
|
- SilverSight.Blitter6502OISC, YangMillsPerformance, WorkloadTestbench, Rollup
|
|
- SilverSight.CollectiveIntelligence.CostTransparency
|
|
|
|
---
|
|
|
|
## What Changed
|
|
|
|
| Before | After |
|
|
|--------|-------|
|
|
| 3 monolithic libraries | 14 standalone modules |
|
|
| SilverSightFormal (~50 roots) | Split into 9 focused modules |
|
|
| SilverSightRRC (~50 roots) | Split into PIST, AVM, RRC, BindingSite, Feasible, Misc |
|
|
| Any change rebuilds everything | Change in Braid? Only rebuilds SilverSightBraid |
|
|
| Circular import risk | Clear layered dependency graph |
|
|
|
|
## Build Commands
|
|
|
|
```bash
|
|
# Build everything
|
|
lake build
|
|
|
|
# Build individual modules
|
|
lake build SilverSightNumerics
|
|
lake build SilverSightBraid
|
|
lake build SilverSightHachimoji
|
|
lake build SilverSightPIST
|
|
lake build SilverSightAVM
|
|
lake build SilverSightRRC
|
|
# etc.
|
|
```
|