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 @@
 </p>
 
 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<br/>M_{k+1} = Quant(Jump(M_k XOR sample))<br/>Use: O(1) discrete Picard shortcut"]:::proposal
         OISC["Equation Type: One-Instruction Logic<br/>4-gate / CMYK scalar update<br/>Use: minimal executable control layer"]:::proposal
         FPGA["Equation Type: LUT/BRAM Search Substrate<br/>BRAM = route memory, LUT = local transition law<br/>Use: hardware search engine"]:::keep
-        TOOLLAW["Equation Type: Toolchain Law<br/>Lean owns logic; Rust owns boundary; Python relays<br/>Use: prevent hidden logic at system boundary"]:::keep
+        TOOLLAW["Equation Type: Toolchain Law<br/>Lean owns all logic and decisions; Rust is boundary shim only; Python relays I/O<br/>Use: prevent hidden logic at system boundary"]:::keep
         RUST["Equation Type: Rust Gimbal<br/>libftdi / hardware I/O bridge<br/>Use: permanent fix over kernel roulette"]:::keep
         VERILOG["Equation Type: Bitstream Boundary<br/>Verilog/bitstream must be generated/proven/audited<br/>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.
 
 ---