From c54cf937cec75d76f34547164d9e060f546a35c5 Mon Sep 17 00:00:00 2001 From: allaunthefox Date: Wed, 8 Jul 2026 07:45:01 +0800 Subject: [PATCH] Add module decomposition analysis --- MODULE_DECOMPOSITION.md | 273 ++++++++++++++++++++++++++++++++++++++++ 1 file changed, 273 insertions(+) create mode 100644 MODULE_DECOMPOSITION.md diff --git a/MODULE_DECOMPOSITION.md b/MODULE_DECOMPOSITION.md new file mode 100644 index 00000000..e9ce57b7 --- /dev/null +++ b/MODULE_DECOMPOSITION.md @@ -0,0 +1,273 @@ +# 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.