From eafbee22b7251e735ba8637f86f2e4f4872f9eac Mon Sep 17 00:00:00 2001 From: Brandon Schneider Date: Tue, 26 May 2026 22:40:03 -0500 Subject: [PATCH] =?UTF-8?q?fix(arch):=20enforce=20Lean-first=20hierarchy?= =?UTF-8?q?=20across=20project=20=E2=80=94=20remove=20all=20secondary-Lean?= =?UTF-8?q?=20language?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Project-wide sweep to find and fix every place Lean was treated as secondary, optional, or subordinate to Python/Rust. The invariant: Lean is the source of truth. Python and Rust are extraction targets only; they contain no logic, no invariant checks, no decisions. Changes: 1-Distributed-Systems/ene/src/lib.rs - CRITICAL: Remove 'Rust is the canonical implementation language for operational components' — replace with correct extraction-target framing 1-Distributed-Systems/agents/claw/README.md - Remove 'canonical implementation lives in rust/' and 'source of truth is ultraworkers/claw-code' blanket claims — scope to CLI binary only; add Research Stack domain-logic note (Lean is source of truth per AGENTS.md) - 'canonical Rust workspace' → 'Rust workspace (I/O extraction target)' 1-Distributed-Systems/agents/claw/src/Tool.py - 'Python-first porting summary' → 'Lean-to-Python extraction summary' 1-Distributed-Systems/agents/claw/src/projectOnboardingState.py - python_first: bool = True → lean_first: bool = True (Lean always leads) 6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md - CRITICAL: 'Python first (reference) ... Lean-formal next' → correct order: Lean specification first, Python extraction shim, Verilog hardware extraction 6-Documentation/docs/recovered/geocognition_equation_types_map.mmd - 'Lean owns logic; Rust owns boundary' → 'Lean owns all logic and decisions; Rust is boundary shim only' 6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md - 'Python implementation ... Lean formalization' → 'Lean specification (source of truth) ... Python extraction shim' 6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md - 'reference specification for the Python implementation' → 'source of truth; Python is an extraction shim against this spec' 6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md - 'Python reference implementation' → 'Python extraction shim' (×2) 5-Applications/scripts/snn/README.md - 'deterministic Python reference' → 'Python extraction shim / golden-vector harness'; add TODO(lean-port) note; RTL must match 'Python shim (pending Lean golden vector)' not 'Python reference' 6-Documentation/docs/METAPROBE_APPROACH.md - 'DeltaGCLCompression.lean — Lean implementation / scripts/delta_gcl_encoder.py — Python reference implementation' → Lean is source of truth / Python is extraction shim Generated with Devin (https://cli.devin.ai/docs) Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com> --- 1-Distributed-Systems/agents/claw/README.md | 5 +++-- 1-Distributed-Systems/agents/claw/src/Tool.py | 2 +- .../agents/claw/src/projectOnboardingState.py | 2 +- 1-Distributed-Systems/ene/src/lib.rs | 5 +++-- 5-Applications/scripts/snn/README.md | 7 ++++--- 6-Documentation/docs/METAPROBE_APPROACH.md | 4 ++-- .../geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md | 2 +- 6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md | 4 ++-- .../docs/recovered/geocognition_equation_types_map.mmd | 2 +- .../docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md | 2 +- 6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md | 2 +- 11 files changed, 20 insertions(+), 17 deletions(-) diff --git a/1-Distributed-Systems/agents/claw/README.md b/1-Distributed-Systems/agents/claw/README.md index f64498c3..5a5ab8dc 100644 --- a/1-Distributed-Systems/agents/claw/README.md +++ b/1-Distributed-Systems/agents/claw/README.md @@ -29,14 +29,15 @@

Claw Code is the public Rust implementation of the `claw` CLI agent harness. -The canonical implementation lives in [`rust/`](./rust), and the current source of truth for this repository is **ultraworkers/claw-code**. +The canonical Rust binary lives in [`rust/`](./rust), and the upstream source for this CLI is **ultraworkers/claw-code**. +Note: for Research Stack domain logic (not CLI I/O), Lean is the source of truth per AGENTS.md; Rust is an extraction target. > [!IMPORTANT] > Start with [`USAGE.md`](./USAGE.md) for build, auth, CLI, session, and parity-harness workflows. Make `claw doctor` your first health check after building, use [`rust/README.md`](./rust/README.md) for crate-level details, read [`PARITY.md`](./PARITY.md) for the current Rust-port checkpoint, and see [`docs/container.md`](./docs/container.md) for the container-first workflow. ## Current repository shape -- **`rust/`** — canonical Rust workspace and the `claw` CLI binary +- **`rust/`** — Rust workspace and the `claw` CLI binary (I/O extraction target) - **`USAGE.md`** — task-oriented usage guide for the current product surface - **`PARITY.md`** — Rust-port parity status and migration notes - **`ROADMAP.md`** — active roadmap and cleanup backlog diff --git a/1-Distributed-Systems/agents/claw/src/Tool.py b/1-Distributed-Systems/agents/claw/src/Tool.py index 16b77aa5..d61c9451 100644 --- a/1-Distributed-Systems/agents/claw/src/Tool.py +++ b/1-Distributed-Systems/agents/claw/src/Tool.py @@ -11,5 +11,5 @@ class ToolDefinition: DEFAULT_TOOLS = ( ToolDefinition('port_manifest', 'Summarize the active Python workspace'), - ToolDefinition('query_engine', 'Render a Python-first porting summary'), + ToolDefinition('query_engine', 'Render a Lean-to-Python extraction summary'), ) diff --git a/1-Distributed-Systems/agents/claw/src/projectOnboardingState.py b/1-Distributed-Systems/agents/claw/src/projectOnboardingState.py index 842a8eb6..1359b3f3 100644 --- a/1-Distributed-Systems/agents/claw/src/projectOnboardingState.py +++ b/1-Distributed-Systems/agents/claw/src/projectOnboardingState.py @@ -7,4 +7,4 @@ from dataclasses import dataclass class ProjectOnboardingState: has_readme: bool has_tests: bool - python_first: bool = True + lean_first: bool = True # Lean is always the source of truth; Python/Rust are extraction targets diff --git a/1-Distributed-Systems/ene/src/lib.rs b/1-Distributed-Systems/ene/src/lib.rs index 779ac463..c0bda628 100644 --- a/1-Distributed-Systems/ene/src/lib.rs +++ b/1-Distributed-Systems/ene/src/lib.rs @@ -4,8 +4,9 @@ //! direct_swarm_probe.py, ingest_keys_to_ene.py, migrate_credentials.py, //! propagate_ssh_keys.py //! -//! Per AGENTS.md §Infrastructure: Rust is the canonical implementation -//! language for operational components. Python shims are deprecated. +//! Per AGENTS.md: Lean is the source of truth. Rust is an extraction target +//! for operational I/O components. Python shims are deprecated in favour of Rust, +//! but neither Rust nor Python may contain logic, invariant checks, or decisions. pub mod config; pub mod credentials; diff --git a/5-Applications/scripts/snn/README.md b/5-Applications/scripts/snn/README.md index 757f35b0..ca2b9c49 100644 --- a/5-Applications/scripts/snn/README.md +++ b/5-Applications/scripts/snn/README.md @@ -5,15 +5,16 @@ on import — see "Calibration deltas" below. ## Layout -- [snn_nii_reference.py](snn_nii_reference.py) — deterministic Python reference. Pipeline: - `predict → nii_step (clamp + bounded Δw + decay) → msnn_step (LIF + FAMM-modulated drive) → rgflow_step (3-verdict) → famm_update (saturating + exp decay)`. +- [snn_nii_reference.py](snn_nii_reference.py) — Python extraction shim / golden-vector harness. + Pipeline: `predict → nii_step (clamp + bounded Δw + decay) → msnn_step (LIF + FAMM-modulated drive) → rgflow_step (3-verdict) → famm_update (saturating + exp decay)`. Writes per-record JSONL with SHA-tagged hash for golden-vector compare. + `TODO(lean-port)`: Port pipeline logic to Lean; Python remains I/O harness only. - [generate_snn_vectors.py](generate_snn_vectors.py) — 4-phase synthetic stream (stable / drift / repeated bad / near-miss osc) OR pulls from a `uc_records.jsonl` topology18 stream. - [snn_test_config.json](snn_test_config.json) — Q8 fixed-point + thresholds. - RTL siblings live at [4-Infrastructure/hardware/tangnano9k/rtl/](../../hardware/tangnano9k/rtl/) and must - bit-match this Python reference. + bit-match this Python shim (pending Lean golden vector). ## Quick start diff --git a/6-Documentation/docs/METAPROBE_APPROACH.md b/6-Documentation/docs/METAPROBE_APPROACH.md index f436efc1..ffc3e2cb 100644 --- a/6-Documentation/docs/METAPROBE_APPROACH.md +++ b/6-Documentation/docs/METAPROBE_APPROACH.md @@ -415,8 +415,8 @@ def retrieveCompressedMetadata (ids : List RecordId) : List GCLManifest := - **AGENTS.md v2.1** — Anti-Drift Evidence Standards - **DELTA_GCL_COMPRESSION_LANGUAGE_AGNOSTIC.md** — Complete specification -- **DeltaGCLCompression.lean** — Lean implementation -- **scripts/delta_gcl_encoder.py** — Python reference implementation +- **DeltaGCLCompression.lean** — Lean source of truth (specification and implementation) +- **scripts/delta_gcl_encoder.py** — Python extraction shim (I/O harness against the Lean spec) --- diff --git a/6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md b/6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md index 728b478c..f1d8fe4c 100644 --- a/6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md +++ b/6-Documentation/docs/geometry/GEOMETRY_TAXONOMY_FOR_NLOCAL_ADAPTATION.md @@ -209,7 +209,7 @@ We classify each geometry format on two independent axes: ### What can be wired as-is: 1. **`geometry_noneuclidean.py`** — its log-PHI and logit functions become subroutines in the Level 4 plugin. -2. **`GWLKernel.lean`** — its metric tensor and geodesic step formulas become the reference specification for the Python implementation. +2. **`GWLKernel.lean`** — its metric tensor and geodesic step formulas are the source of truth; Python is an extraction shim against this spec. 3. **`topological_tape_machine.py`** — operates at a higher layer; unchanged interface. 4. **`tsm_perpetual_manifold.v`** — unchanged; the geometry layer feeds it, it doesn't compute geometry. 5. **`Physics/*.lean`** — unchanged; serves as the invariant boundary. diff --git a/6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md b/6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md index 0c2f68c2..49871258 100644 --- a/6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md +++ b/6-Documentation/docs/protocols/TM_MCP_SPECIFICATION.md @@ -781,7 +781,7 @@ src/tm_mcp/ ### 7.2 Data Structures (Pseudocode) ```python -# Python reference implementation +# Python extraction shim (Lean spec is source of truth; this is I/O scaffolding only) from dataclasses import dataclass from typing import List, Optional, Dict, Union @@ -1132,7 +1132,7 @@ class BenchmarkCompression(unittest.TestCase): **Next Steps:** 1. Implement `TMMCP/` Lean modules with `#eval` verification -2. Create Python reference implementation (`infra/tm_mcp/`) +2. Create Python extraction shim (`infra/tm_mcp/`) from the Lean spec 3. Validate MVP channels against synthetic data 4. Run `lake build` and add to CI 5. Measure compression ratios and reconstruction error for benchmark suite diff --git a/6-Documentation/docs/recovered/geocognition_equation_types_map.mmd b/6-Documentation/docs/recovered/geocognition_equation_types_map.mmd index d3b9ce13..b60bd14e 100644 --- a/6-Documentation/docs/recovered/geocognition_equation_types_map.mmd +++ b/6-Documentation/docs/recovered/geocognition_equation_types_map.mmd @@ -107,7 +107,7 @@ flowchart TD BLIT["Equation Type: Bit-Blit Update
M_{k+1} = Quant(Jump(M_k XOR sample))
Use: O(1) discrete Picard shortcut"]:::proposal OISC["Equation Type: One-Instruction Logic
4-gate / CMYK scalar update
Use: minimal executable control layer"]:::proposal FPGA["Equation Type: LUT/BRAM Search Substrate
BRAM = route memory, LUT = local transition law
Use: hardware search engine"]:::keep - TOOLLAW["Equation Type: Toolchain Law
Lean owns logic; Rust owns boundary; Python relays
Use: prevent hidden logic at system boundary"]:::keep + TOOLLAW["Equation Type: Toolchain Law
Lean owns all logic and decisions; Rust is boundary shim only; Python relays I/O
Use: prevent hidden logic at system boundary"]:::keep RUST["Equation Type: Rust Gimbal
libftdi / hardware I/O bridge
Use: permanent fix over kernel roulette"]:::keep VERILOG["Equation Type: Bitstream Boundary
Verilog/bitstream must be generated/proven/audited
Use: suspect until linked to Lean source of truth"]:::audit end diff --git a/6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md b/6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md index d721a4f7..32d6d421 100644 --- a/6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md +++ b/6-Documentation/docs/semantics/HYPER_DIMENSIONAL_PHYSICS_INTRO.md @@ -553,4 +553,4 @@ The coordinates are computed, not stored. The decoder reconstructs them from `n` --- -*End of walkthrough. The Python implementation is in `pist_alpha_extended.py`. The Lean formalization is in `ExtendedManifoldEncoding.lean`.* +*End of walkthrough. The Lean specification is in `ExtendedManifoldEncoding.lean` (source of truth). The Python extraction shim is in `pist_alpha_extended.py`.* diff --git a/6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md b/6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md index f9b26030..285542e9 100644 --- a/6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md +++ b/6-Documentation/docs/specs/ENE_MEMORY_ATLAS_SPEC.md @@ -368,7 +368,7 @@ Following the MOIM project autopsy's principle (separate REAL from DREAM): | MCP server fronting atlas | **NOT YET** | open work | | Tang Nano 9K FPGA target | **NOT YET (local)** | Kimi has it; local does not | -**The combination's first real deliverable** = MCP server that exposes the existing local pieces (voxel_key lookup, regime-bin scan, Q0_16 read/write through tardy BFT, settlement state filter) over a single protocol. The MOIM-side fractal hash and Dless Ω can land as Python first (reference per `ene_ingestion_engine.py`), Lean-formal next (`ENEDatabase.lean`, `DlessScalar.lean` ports), Verilog last (Tang Nano 9K, deferred). +**The combination's first real deliverable** = MCP server that exposes the existing local pieces (voxel_key lookup, regime-bin scan, Q0_16 read/write through tardy BFT, settlement state filter) over a single protocol. The MOIM-side fractal hash and Dless Ω must be specified in Lean first (`ENEDatabase.lean`, `DlessScalar.lean`), with Python as an extraction shim (reference I/O: `ene_ingestion_engine.py`) and Verilog as the hardware extraction target (Tang Nano 9K, deferred). Lean is the source of truth; Python and Verilog are extraction targets only. ---