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>
**CRITICAL fixes**
- Header: note UNIVERSAL_SUBSTRATE_ROADMAP.md no longer exists on disk;
add note that TODO_MAP.md may lag this file
- §11: replace dead cross-reference with accurate statement; mark full
census reconstruction as Phase 0 deliverable
- Phase 0: split into completed infrastructure vs pending Lean work;
explicitly note `USTSM_State` does not yet exist in any Lean file
**ERROR fixes**
- §1: retract unverified "2,634 models" figure; replace with measured
1,126 ingested equation rows (source: equations.csv 2026-05-18)
- §6 Invariant 7: clarify Q0_64 universality is a Phase 0-1 design
goal, not a current enforced fact; note Bind.lean uses Q16_16
exclusively by design ("all values require integer component for
gradient computation") — no contradiction, different scopes
- §8: expand Semantics/Semantics description to reflect 946+ entries
(not a handful of named modules); update §4-Infrastructure/infra/
description to reflect Rust-only state (Python shims removed)
- §12 Credential Gateway: remove reference to deleted credential_server.py;
credit rs-surface binary and credential.rs module
**WARNING fixes**
- §10 FPGA Hardware: change ✅ Synthesized → 🔄 Bitstream ready; add
"live hardware receipt pending" caveat
- Phase 4 heading: rename to clarify concurrent-with-Phases-2-3; add
explanatory note
**BLOCKED annotation**
- Immediate action #8 (Flash Tang Nano 9K): mark as blocked on physical
board + USB programmer
Generated with [Devin](https://cli.devin.ai/docs)
Co-Authored-By: Devin <158243242+devin-ai-integration[bot]@users.noreply.github.com>
- cupfox-config.nix: add Open WebUI container with chat.researchstack.info proxy,
gather-metrics service/timer, rclone, and tmpfiles for persistent storage
- Lean semantics: reduce axiom count from 109 to 18 across 10 files;
FixedPoint now 0 axioms, 0 sorries with 12 theorems
- Documentation: update AGENTS.md with current axiom/sorry counts and
FixedPoint status; refine bind signature
- Add topology scripts, CGA/FAMM/GeneticOptimizer/MMRFAMM Lean modules,
devcontainer config, MEMORY.md, and Modelfile
Provide two lists for clean system recovery:
- frt-core-packages.txt: 90 packages required to build, verify, and run
the Research Stack (VITAL + NEEDED tiers). Install first on fresh system.
- personal-packages.txt: ~200 packages that are NOT required for FRT work.
These are quality-of-life, niche domain, or redundant tools. Safe to remove
for a clean research environment; reinstall on demand.
Total potential savings: ~3-5GB by removing personal tier.
Also includes the full 391-package master inventory with per-package
justifications in software_inventory_2026-05-13.md.
