From 6d2136c32842cca85a6ae1cf892d8e3c011e2dbb Mon Sep 17 00:00:00 2001
From: allaunthefox <allaunthefox@users.noreply.github.com>
Date: Wed, 8 Jul 2026 07:42:39 +0800
Subject: [PATCH] Extract monolithic lakefile into 14 standalone module targets

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.
---
 MODULE_MAP.md | 184 ++++++++++++++++++++++++++++++++++++++++++++++++++
 lakefile.lean | 160 ++++++++++++++++++++++++++++++-------------
 2 files changed, 296 insertions(+), 48 deletions(-)
 create mode 100644 MODULE_MAP.md

diff --git a/MODULE_MAP.md b/MODULE_MAP.md
new file mode 100644
index 00000000..c9b8f8be
--- /dev/null
+++ b/MODULE_MAP.md
@@ -0,0 +1,184 @@
+# 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.
+```
diff --git a/lakefile.lean b/lakefile.lean
index ecffbbac..25c24ee4 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -4,75 +4,84 @@ open System
 
 package «SilverSight» where
   leanOptions := #[
-    ⟨`pp.unicode.fun, true⟩ -- pretty-prints `fun a ↦ b`
+    ⟨`pp.unicode.fun, true⟩
   ]
-  -- Add any additional package configuration options here
 
+-- ─── Layer 0: Core Foundation ────────────────────────────────────────────────
 @[default_target]
 lean_lib «SilverSightCore» where
-  -- Add any library configuration options here
   srcDir := "Core"
   roots := #[`SilverSightCore, `SilverSight.FixedPoint, `SilverSight.Semantics.Schema, `SilverSight.Semantics.Layout, `SilverSight.Semantics.WireFormat, `SilverSight.Semantics.View, `SilverSight.Semantics.LayoutBridge, `SilverSight.Semantics.CanalLayout]
 
-lean_lib «SilverSightFormal» where
+-- ─── Layer 1: Numerics & Fixed-Point ─────────────────────────────────────────
+lean_lib «SilverSightNumerics» where
   srcDir := "formal"
   roots := #[
     `CoreFormalism.FixedPoint,
-    `SilverSight.PrimeLut,
-    `SilverSight.FixedPointBridge,
     `CoreFormalism.Tactics,
     `CoreFormalism.Q16_16Numerics,
+    `SilverSight.PrimeLut,
+    `SilverSight.FixedPointBridge
+  ]
+
+-- ─── Layer 2: Canal / Dynamic Infrastructure ─────────────────────────────────
+lean_lib «SilverSightCanal» where
+  srcDir := "formal"
+  roots := #[
     `CoreFormalism.DynamicCanal,
-    `CoreFormalism.Bind,
+    `CoreFormalism.Bind
+  ]
+
+-- ─── Layer 3a: Braid Theory ──────────────────────────────────────────────────
+lean_lib «SilverSightBraid» where
+  srcDir := "formal"
+  roots := #[
     `CoreFormalism.BraidBracket,
     `CoreFormalism.BraidStrand,
     `CoreFormalism.BraidCross,
     `CoreFormalism.BraidField,
     `CoreFormalism.BraidStateN,
+    `CoreFormalism.BraidEigensolid,
+    `CoreFormalism.BraidSpherionBridge,
+    `CoreFormalism.ContractedCrossStep
+  ]
+
+-- ─── Layer 3b: Sidon / Number Theory ─────────────────────────────────────────
+lean_lib «SilverSightSidon» where
+  srcDir := "formal"
+  roots := #[
     `CoreFormalism.SidonSets,
     `CoreFormalism.SieveLemmas,
     `CoreFormalism.InteractionGraphSidon,
-    `CoreFormalism.BraidEigensolid,
-    `CoreFormalism.ContractedCrossStep,
-    `CoreFormalism.BraidSpherionBridge,
+    `CoreFormalism.CRTSidon,
+    `CoreFormalism.CRTSidonN,
     `CoreFormalism.E8Sidon,
     `CoreFormalism.EisensteinSeries,
-    `CoreFormalism.ComplexProjectiveSpace,
     `CoreFormalism.GoormaghtighEnumeration,
+    `CoreFormalism.StrandCapacityBound
+  ]
+
+-- ─── Layer 3c: Hachimoji DNA Encoding ────────────────────────────────────────
+lean_lib «SilverSightHachimoji» where
+  srcDir := "formal"
+  roots := #[
     `CoreFormalism.HachimojiBase,
     `CoreFormalism.HachimojiCodec,
     `CoreFormalism.HachimojiLUT,
     `CoreFormalism.HachimojiBridging,
     `CoreFormalism.HachimojiManifoldAxiom,
-    `CoreFormalism.ChentsovFinite,
-    `CoreFormalism.HopfFibration,
-    `CoreFormalism.StrandCapacityBound,
-    `CoreFormalism.CRTSidon,
-    `CoreFormalism.CRTSidonN,
-    `SilverSight.AngrySphinx,
-    `SilverSight.BlockCoprimeDensity,
-    `SilverSight.CollatzBraid,
-    `SilverSight.GoldenSpiral,
-    `SilverSight.GCCL,
-    `SilverSight.WireFormat,
-    `SilverSight.ProductSchema,
-    `SilverSight.ProductWireFormat,
-    `SilverSight.Receipt,
-    `BindingSite.BindingSiteTypes,
-    `BindingSite.BindingSiteHachimoji,
-    `BindingSite.BindingSiteEntropy,
-    `BindingSite.BindingSiteCodec
-  ]
-
-lean_lib «SilverSightRRC» where
-  srcDir := "formal"
-  roots := #[
     `SilverSight.HachimojiN8,
     `SilverSight.HachimojiN8Bridge,
     `SilverSight.HachimojiCharClass,
     `SilverSight.PhiDNALayout,
     `SilverSight.PhiConsistency,
-    `SilverSight.PhiPipelineReceipt,
+    `SilverSight.PhiPipelineReceipt
+  ]
+
+-- ─── Layer 4: PIST / Spectral Classification ─────────────────────────────────
+lean_lib «SilverSightPIST» where
+  srcDir := "formal"
+  roots := #[
     `SilverSight.PIST.Spectral,
     `SilverSight.PIST.SpectralN,
     `SilverSight.PIST.MatrixN,
@@ -93,14 +102,13 @@ lean_lib «SilverSightRRC» where
     `SilverSight.PIST.SidonAdapter,
     `SilverSight.PIST.WeightCandidateGen,
     `SilverSight.PIST.UnitDistCandidateGen,
-    `SilverSight.PIST.CMYKColoringCore,
-    `SilverSight.RRCLogogramProjection,
-    `SilverSight.ReceiptCore,
-    `SilverSight.RRC.Emit,
-    `SilverSight.RRC.ReceiptDensity,
-    `SilverSight.RRC.PolyFactorIdentity,
-    `SilverSight.RRC.EntropyCandidates,
-    `SilverSight.RRC.Q16_16Manifold,
+    `SilverSight.PIST.CMYKColoringCore
+  ]
+
+-- ─── Layer 5: AVM Instruction Set Architecture ───────────────────────────────
+lean_lib «SilverSightAVM» where
+  srcDir := "formal"
+  roots := #[
     `SilverSight.AVMIsa.Types,
     `SilverSight.AVMIsa.Value,
     `SilverSight.AVMIsa.Instr,
@@ -109,7 +117,54 @@ lean_lib «SilverSightRRC» where
     `SilverSight.AVMIsa.TypeCheck,
     `SilverSight.AVMIsa.TypeSafety,
     `SilverSight.AVMIsa.Run,
-    `SilverSight.AVMIsa.Emit,
+    `SilverSight.AVMIsa.Emit
+  ]
+
+-- ─── Layer 6: RRC Receipt Pipeline ───────────────────────────────────────────
+lean_lib «SilverSightRRC» where
+  srcDir := "formal"
+  roots := #[
+    `SilverSight.RRCLogogramProjection,
+    `SilverSight.ReceiptCore,
+    `SilverSight.RRC.Emit,
+    `SilverSight.RRC.ReceiptDensity,
+    `SilverSight.RRC.PolyFactorIdentity,
+    `SilverSight.RRC.EntropyCandidates,
+    `SilverSight.RRC.Q16_16Manifold,
+    `RRCLib.RRCEmit
+  ]
+
+-- ─── Layer 7: Binding Site Codec ─────────────────────────────────────────────
+lean_lib «SilverSightBindingSite» where
+  srcDir := "formal"
+  roots := #[
+    `BindingSite.BindingSiteTypes,
+    `BindingSite.BindingSiteHachimoji,
+    `BindingSite.BindingSiteEntropy,
+    `BindingSite.BindingSiteCodec
+  ]
+
+-- ─── Layer 8: Optimisation / Feasible Set ────────────────────────────────────
+lean_lib «SilverSightFeasible» where
+  srcDir := "formal"
+  roots := #[
+    `SilverSight.FeasibleSet.Theorem,
+    `SilverSight.FeasibleSet.QUBORelaxation
+  ]
+
+-- ─── Standalone / Miscellaneous ──────────────────────────────────────────────
+lean_lib «SilverSightMisc» where
+  srcDir := "formal"
+  roots := #[
+    `SilverSight.AngrySphinx,
+    `SilverSight.BlockCoprimeDensity,
+    `SilverSight.CollatzBraid,
+    `SilverSight.GoldenSpiral,
+    `SilverSight.GCCL,
+    `SilverSight.WireFormat,
+    `SilverSight.ProductSchema,
+    `SilverSight.ProductWireFormat,
+    `SilverSight.Receipt,
     `SilverSight.AdjugateMatrix,
     `SilverSight.ChiralClockModel,
     `SilverSight.ColdReviewer,
@@ -119,10 +174,17 @@ lean_lib «SilverSightRRC» where
     `SilverSight.YangMillsPerformance,
     `SilverSight.WorkloadTestbench,
     `SilverSight.Rollup,
-    `SilverSight.FeasibleSet.Theorem,
-    `SilverSight.FeasibleSet.QUBORelaxation,
-    `SilverSight.CollectiveIntelligence.CostTransparency,
-    `RRCLib.RRCEmit
+    `SilverSight.CollectiveIntelligence.CostTransparency
+  ]
+
+-- ─── Geometry (standalone) ───────────────────────────────────────────────────
+lean_lib «SilverSightGeometry» where
+  srcDir := "formal"
+  roots := #[
+    `CoreFormalism.ComplexProjectiveSpace,
+    `CoreFormalism.ChentsovFinite,
+    `CoreFormalism.HopfFibration,
+    `CoreFormalism.AutoProof
   ]
 
 /-! Dead code archived 2026-07-03. See archive/dead_code_2026-07-03/README.md
@@ -134,6 +196,8 @@ lean_lib «SilverSightRRC» where
     - SilverSight/FeasibleSet/TestChain.lean
 -/
 
+-- ─── Executables ─────────────────────────────────────────────────────────────
+
 lean_exe «rrc-emit-fixture» where
   root := `RrcEmitFixture
   srcDir := "exe"