mirror of
https://github.com/allaunthefox/Research-Stack.git
synced 2026-07-31 03:05:21 +00:00
273 lines
9.4 KiB
Markdown
273 lines
9.4 KiB
Markdown
# Research-Stack MODULE_DECOMPOSITION.md
|
|
|
|
**Date:** 2026-07-08
|
|
**Status:** Analysis complete — 12 proposed standalone modules
|
|
|
|
---
|
|
|
|
## Current State
|
|
|
|
- **Total .lean files:** 925 (in `0-Core-Formalism/lean/Semantics/`)
|
|
- **Sorry count:** 76 across 29 files
|
|
- **Foundation:** `Semantics.FixedPoint` imported by 452 files
|
|
- **Second layer:** `Semantics.Bind` imported by 71 files
|
|
- **Third layer:** `Semantics.DynamicCanal` imported by 25 files
|
|
- **Current lakefile:** `lakefile.toml` (monolithic, all roots in one target)
|
|
|
|
---
|
|
|
|
## Proposed Module Groups (12 modules)
|
|
|
|
### Module 1: `rs_core` — Foundation Axioms
|
|
**Files:** 3 | **Sorry:** 19 | **External deps:** Mathlib (Manifold, Probability, Analysis)
|
|
|
|
| File | Path |
|
|
|------|------|
|
|
| BindAxioms | Core/ |
|
|
| InformationManifold | Core/ |
|
|
| T1_Coherence | Core/ |
|
|
|
|
**Internal deps:** None (this is the root)
|
|
**Notes:** 19 sorrys in T1_Coherence (12) and InformationManifold (7). These are the "brain" — the SIM framework axioms. T1_Coherence v2.0 replaced vacuous `True := by trivial` with honest `sorry`.
|
|
|
|
---
|
|
|
|
### Module 2: `rs_numerics` — Fixed-Point & Q16_16 Arithmetic
|
|
**Files:** ~15 | **Sorry:** 0 | **External deps:** Mathlib (Data.Nat, Data.Int, Data.Real)
|
|
|
|
Core files (imported by 452+ others):
|
|
- FixedPoint (the single most imported file)
|
|
- Q16_16Numerics
|
|
- Toolkit
|
|
- PhysicsScalarBridge
|
|
- RegimeCore
|
|
|
|
**Internal deps:** rs_core (BindAxioms)
|
|
**Notes:** This is the true foundation — almost everything imports FixedPoint. Must be extracted first.
|
|
|
|
---
|
|
|
|
### Module 3: `rs_bind` — Bind Infrastructure
|
|
**Files:** ~20 | **Sorry:** 0 | **External deps:** Lean.Data.Json, Mathlib
|
|
|
|
Core files:
|
|
- Bind (imported by 71 files)
|
|
- DynamicCanal (imported by 25 files)
|
|
- LocalDerivative
|
|
- OrthogonalAmmr
|
|
- ManifoldStructures
|
|
|
|
**Internal deps:** rs_core, rs_numerics
|
|
**Notes:** Bind and DynamicCanal are the infrastructure layer that most domain modules depend on.
|
|
|
|
---
|
|
|
|
### Module 4: `rs_braid` — Braid Theory
|
|
**Files:** ~13 | **Sorry:** 0 | **External deps:** Mathlib
|
|
|
|
Files (prefix `Braid*`):
|
|
- BraidBracket, BraidStrand, BraidCross, BraidField, BraidStateN
|
|
- BraidEigensolid, BraidSpherionBridge
|
|
- + related files
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Self-contained cluster with 22 internal imports. Clear boundary.
|
|
|
|
---
|
|
|
|
### Module 5: `rs_physics` — Physics & Conservation Laws
|
|
**Files:** ~30 | **Sorry:** 1 | **External deps:** Mathlib (Analysis, Topology)
|
|
|
|
Subdirectories: `Physics/` (24), `PhysicsData/` (1), `FNWH/` (4)
|
|
Key files:
|
|
- Conservation, Boundary, Interaction, Projection
|
|
- BurgersBridge, BurgersPDE
|
|
- DESIInvariant, DESIModelProjection
|
|
- NBody, QCLEnergy, RydbergExperimentalTest
|
|
- LHCb_BToKStarMuMu (real LHCb data!)
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Contains actual experimental data references (LHCb). The BurgersPDE files are imported by 13 others.
|
|
|
|
---
|
|
|
|
### Module 6: `rs_extensions` — Biological & Ecological Extensions
|
|
**Files:** 105 | **Sorry:** 0 | **External deps:** Mathlib (Analysis, SpecialFunctions)
|
|
|
|
All files in `Semantics/Extensions/`:
|
|
- Biological laws (70+ files: BioComplexSystems, CellularGrowthLaws, etc.)
|
|
- Ecological dynamics (EcologicalBehaviors, EcologicalNetworkDynamics, etc.)
|
|
- Evolutionary dynamics (EvolutionaryLandscapeDynamics, etc.)
|
|
- Cognitive/social dynamics (CognitiveLearningDynamics, SocialCognitiveDynamics, etc.)
|
|
- Physics-adjacent (HarmonicKinkPlasmaManifold, HyperbolicStateSurface, etc.)
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Largest module (105 files). Could be further split into Bio/Ecology/Evolution/Cognitive sub-modules. Zero sorrys — these are all statement-only (axiom/theorem definitions without proof obligations).
|
|
|
|
---
|
|
|
|
### Module 7: `rs_hcmmr` — HCMMR Laws & Kernels
|
|
**Files:** 20 | **Sorry:** 0 | **External deps:** Mathlib
|
|
|
|
All in `Semantics/HCMMR/`:
|
|
- Law14 through Law21 (Motion, SignalDetection, Field, Entropy, Observer, etc.)
|
|
- Kernels: HyperEigenSpectrum, BoundaryEigenFire, etc.
|
|
- FAMMScarMemory, SNRAnomalyDetector, PrimeGearCache
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Self-contained law framework. Clear naming convention (Law##).
|
|
|
|
---
|
|
|
|
### Module 8: `rs_hardware` — Hardware & FPGA
|
|
**Files:** 12 | **Sorry:** 0 | **External deps:** None (hardware-level)
|
|
|
|
All in `Semantics/Hardware/`:
|
|
- AdaptiveFabric, AgenticHardware, BitstreamWitness
|
|
- Blitter6502OISC (OISC computer!)
|
|
- EmergencyBootShell/State/Types
|
|
- HardwareExtraction, LaserPathCell
|
|
- TangNano9K/ (3 files — actual FPGA target)
|
|
- NIICore, RGFlowFAMM
|
|
|
|
**Internal deps:** rs_numerics
|
|
**Notes:** Contains TangNano9K FPGA code. Self-contained hardware layer.
|
|
|
|
---
|
|
|
|
### Module 9: `rs_nii` — NIICore Cognitive Architecture
|
|
**Files:** 20 | **Sorry:** 0 | **External deps:** Mathlib
|
|
|
|
All in `Semantics/NIICore/`:
|
|
- CognitiveLoadIntegration, DifferentialAttentionMorphing
|
|
- HierarchicalController, MetaLearning
|
|
- MorphicCoreId, MorphicFieldCategory, MorphingTriggers
|
|
- SemanticAnalysis, SemanticCapabilitySystem, SemanticRGFlow
|
|
- UncertaintyQuantification, Verification, etc.
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Self-contained cognitive architecture. Clear internal naming.
|
|
|
|
---
|
|
|
|
### Module 10: `rs_genomic` — Genomic Compression
|
|
**Files:** 6 | **Sorry:** 0 | **External deps:** Mathlib
|
|
|
|
All in `Semantics/GenomicCompression/`:
|
|
- Components, Compression, Field, NonDriftProof, Theorems, Types
|
|
|
|
Plus `Semantics/Biology/` (3 files):
|
|
- BioRxivFormalization, QuaternionGenomic, RGFlowBioinformatics
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Small, focused module. NonDriftProof name suggests drift-prevention guarantees.
|
|
|
|
---
|
|
|
|
### Module 11: `rs_testing` — Tests & Benchmarks
|
|
**Files:** ~45 | **Sorry:** 0 | **External deps:** Mathlib
|
|
|
|
- `Semantics/Testing/` (39 files): adversarial, baseline, conservation, GPU, benchmark tests
|
|
- `Semantics/Benchmarks/` (2 files): Grid17x17, HadwigerNelson
|
|
- `Semantics/Toybox/` (4 files): HierarchicalBinding, ObserverAngle, etc.
|
|
|
|
**Internal deps:** rs_numerics (FixedPointTest, etc.)
|
|
**Notes:** Test infrastructure. Should be buildable but not imported by other modules.
|
|
|
|
---
|
|
|
|
### Module 12: `rs_scaffold` — Extension Scaffold
|
|
**Files:** 36 | **Sorry:** 1 | **External deps:** Mathlib
|
|
|
|
All in `ExtensionScaffold/`:
|
|
- **Compression/** (14 files): AdaptiveBlock, CellCore, CodingCost, HutterContext, etc.
|
|
- **Temporal/** (9 files): CommitClock, MetabolicTvi, OMT, RegenerationPolicy, etc.
|
|
- **ENE/** (5 files): SemanticLinter, SessionArchive, AutoImported, etc.
|
|
- **Physics/** (2 files): NBody, VideoWeirdMachine
|
|
- **Topology/** (2 files): PlasmaTopology, Wormhole
|
|
- **Thermodynamics/** (1 file): ThroatPhysics
|
|
- **Decoherence/** (1 file): HistoryTvi
|
|
- **Seed/** (1 file): uSeed
|
|
- MissingProofsTest (1 file)
|
|
|
|
**Internal deps:** rs_numerics, rs_bind
|
|
**Notes:** Already well-organized by subdirectory. Compression/ is the densest cluster.
|
|
|
|
---
|
|
|
|
## Orphan / Unclassified Files
|
|
|
|
These files in `Semantics/` (flat) don't clearly belong to any cluster:
|
|
|
|
| File | Imports | Notes |
|
|
|------|---------|-------|
|
|
| SSMS | FixedPoint | Standalone |
|
|
| ShellModel | FixedPoint | Standalone |
|
|
| Canon | FixedPoint | Standalone |
|
|
| GoldenSpiral | FixedPoint | Standalone |
|
|
| CollatzBraid | FixedPoint | Standalone |
|
|
| Various `test_native_decide` | None | Test file |
|
|
|
|
**Recommendation:** These go into rs_numerics or a rs_misc catch-all.
|
|
|
|
---
|
|
|
|
## Dependency Graph
|
|
|
|
```
|
|
rs_core (3 files, 19 sorrys)
|
|
└─► rs_numerics (~15 files, 0 sorrys)
|
|
├─► rs_bind (~20 files)
|
|
│ ├─► rs_braid (~13 files)
|
|
│ ├─► rs_physics (~30 files)
|
|
│ ├─► rs_extensions (105 files)
|
|
│ ├─► rs_hcmmr (20 files)
|
|
│ ├─► rs_hardware (12 files)
|
|
│ ├─► rs_nii (20 files)
|
|
│ ├─► rs_genomic (9 files)
|
|
│ └─► rs_scaffold (36 files)
|
|
└─► rs_testing (~45 files) [leaf, not imported by others]
|
|
```
|
|
|
|
---
|
|
|
|
## Sorry Distribution
|
|
|
|
| Module | Files | Sorry Count | Files with Sorry |
|
|
|--------|-------|-------------|-----------------|
|
|
| rs_core | 3 | 19 | 2 |
|
|
| rs_numerics | ~15 | 0 | 0 |
|
|
| rs_bind | ~20 | 0 | 0 |
|
|
| rs_braid | ~13 | 0 | 0 |
|
|
| rs_physics | ~30 | 1 | 1 |
|
|
| rs_extensions | 105 | 0 | 0 |
|
|
| rs_hcmmr | 20 | 0 | 0 |
|
|
| rs_hardware | 12 | 0 | 0 |
|
|
| rs_nii | 20 | 0 | 0 |
|
|
| rs_genomic | 9 | 0 | 0 |
|
|
| rs_testing | ~45 | 0 | 0 |
|
|
| rs_scaffold | 36 | 1 | 1 |
|
|
| **Total** | **~328** | **21** | **4** |
|
|
|
|
**Note:** 55 sorrys are in the flat `Semantics/` directory files not yet assigned to modules. The 76 total sorry count includes files that need further classification.
|
|
|
|
---
|
|
|
|
## Recommended Extraction Order
|
|
|
|
1. **rs_numerics** first (FixedPoint is imported by 452 files — everything depends on it)
|
|
2. **rs_core** second (BindAxioms → InformationManifold → T1_Coherence)
|
|
3. **rs_bind** third (Bind + DynamicCanal)
|
|
4. **rs_braid** fourth (clear cluster, easy to extract)
|
|
5. **rs_testing** fifth (leaf module, no downstream deps)
|
|
6. **rs_scaffold** sixth (already organized by subdirectory)
|
|
7. Remaining modules in any order (rs_physics, rs_extensions, rs_hcmmr, rs_hardware, rs_nii, rs_genomic)
|
|
|
|
---
|
|
|
|
## Open Questions
|
|
|
|
1. **Should rs_extensions (105 files) be split further?** Bio/Ecology/Evolution/Cognitive are distinct domains.
|
|
2. **What to do with the 513 flat Semantics/ files?** Many are standalone statements (axiom/theorem). Need per-file import analysis to assign to modules.
|
|
3. **Should sorrys be addressed before or after extraction?** Extracting first makes the sorry boundaries visible.
|
|
4. **The flat Semantics/ files contain ~55 sorrys** — these need classification before final module assignment.
|