All research stack related work and material is folded here, each project subdivided into it's own folders.
Find a file
Brandon Schneider 251ea9d9bf docs: comprehensive infrastructure documentation
Covers:
- 5-node Tailscale mesh (nixos, qfox, 361395-1, racknerd, steamdeck)
- k3s cluster: 7 namespaces, 20+ services, Traefik ingress
- FPGA: Tang Nano 9K, 6-module bitstream, 195.92 MHz
- GPU: RTX 4070, Ollama deepseek-coder-v2:16b
- Lean: 3572 jobs, 10 modules, 8 sorries
- Python: 68/68 tests, HiGHS 8.4ms
- Skills: 111 enabled (6 local, 12 hub, 85 builtin)
- MCP servers: eda, lean, sympy, contextstream, aws
- DNS/TLS: researchstack.info, Porkbun, LE certs
- Key constants: Q16_16, golden angle, baud rate, Kolmogorov
2026-05-29 01:12:18 -05:00
.agents/plugins Consolidate research stack updates 2026-05-05 21:09:48 -05:00
.consolidation-manifests initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
.contextstream chore: rename workspace from nodupelabs to researchstack 2026-05-27 00:46:44 -05:00
.cursor WIP: accumulated changes 2026-05-25 16:24:21 -05:00
.devcontainer devcontainer: replace Alpine base with nixos/nix; add sagemath 2026-05-19 09:40:14 +00:00
.devin feat(skills): extend lean-proof skill with anti-drift rules 2026-05-26 22:52:52 -05:00
.github docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
.kilo/rules chore: rename workspace from nodupelabs to researchstack 2026-05-27 00:46:44 -05:00
.opencode/agents docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
.roo docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
.vscode Stabilize remote proof endpoint and RDS shims 2026-05-25 20:48:25 -05:00
.windsurf docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
0-Core-Formalism feat: particle physics pipeline — LadderBraid, PenguinDecay, RRC, PhysicsPipeline 2026-05-28 19:43:39 -05:00
1-Distributed-Systems fix(arch): enforce Lean-first hierarchy across project — remove all secondary-Lean language 2026-05-26 22:40:03 -05:00
2-Search-Space feat(avm-isa): Goal A — AVMIsa.Emit wires canary → RRC → JSON; clear build red 2026-05-26 21:46:22 -05:00
3-Mathematical-Models chore(manifold): remove orphaned MISC Python tests 2026-05-20 18:50:11 -05:00
4-Infrastructure fix: UART bug (retransmit) + auto-start + LED heartbeat + sim verification 2026-05-28 21:42:11 -05:00
5-Applications fix: reed_solomon_vcn decode_rs return type (tuple → bytes extraction) 2026-05-28 17:35:55 -05:00
6-Documentation docs: comprehensive infrastructure documentation 2026-05-29 01:12:18 -05:00
6-Kernel-Shim Consolidate research stack updates 2026-05-05 21:09:48 -05:00
ai-math-discovery-systems fix: correct Q16_16 add/sub signed/unsigned bug, add missing lemmas 2026-05-18 00:31:44 -05:00
archive/2026-05-26 archive: preserve duplicate PISTMachine search-space copy 2026-05-26 14:30:39 -05:00
data/erdos_famm_solved_scars Add OpenAI unit-distance disproof as Erdos FAMM solved scar 2026-05-20 23:01:41 -05:00
docs Add guide for OpenAI unit-distance disproof as FAMM solve pattern 2026-05-20 23:01:41 -05:00
obsidian-vault docs: add external research import maps 2026-05-20 18:41:21 -05:00
pending/lean_unification chore(pending): move python ENE ContextStream MCP surface into pending quarantine 2026-05-26 17:59:51 -05:00
plugins/substack-connector Consolidate research stack updates 2026-05-05 21:09:48 -05:00
scripts/qc-flag docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 2026-05-26 22:34:46 -05:00
shared-data docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 2026-05-26 22:34:46 -05:00
workspace-config initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
.aider.conf.yml chore: rename workspace from nodupelabs to researchstack 2026-05-27 00:46:44 -05:00
.clinerules docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
.codeiumignore Add workspace load-shedding ignores 2026-05-11 15:53:59 -05:00
.cursorrules docs: sync all editor rules, opencode agents, and sorry audit 2026-05-28 17:53:54 -05:00
.gitattributes WIP: accumulated changes 2026-05-25 16:24:21 -05:00
.gitignore archive: remove dated receipts, experimental probes, and uncompiled prototypes 2026-05-25 16:51:58 -05:00
.gitmodules archive: remove dated receipts, experimental probes, and uncompiled prototypes 2026-05-25 16:51:58 -05:00
.mcp.json Stabilize ENE API and context shim 2026-05-25 21:06:46 -05:00
.pre-commit-config.yaml math-first: fix pre-commit evidence-gate filter bug, polish schema + validator 2026-05-12 04:40:20 +00:00
.python-version Track DeepSeek review receipts and CAD setup tasks 2026-05-11 22:41:44 -05:00
.sops.yaml WIP: accumulated changes 2026-05-25 16:24:21 -05:00
AGENTS.md docs: enforce lean-proof skill + no-float rule in AGENTS.md Ground Rules 2026-05-29 00:06:12 -05:00
ARCHITECTURE.md docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 2026-05-26 22:34:46 -05:00
CHANGELOG.md docs: full documentation + roadmap refresh (2026-05-19) 2026-05-19 09:12:16 +00:00
CITATION.cff Track HCMMR sources and ignore generated mirrors 2026-05-11 21:53:32 -05:00
claims.yaml Merge math-first tooling guardrails 2026-05-11 23:34:48 -05:00
CLAUDE.md chore: rename workspace from nodupelabs to researchstack 2026-05-27 00:46:44 -05:00
CONCEPTS.md WIP: accumulated changes 2026-05-25 16:24:21 -05:00
Containerfile integrate stashed changes: math model data updates + 4 receipt dirs + container config 2026-05-17 12:03:19 -05:00
cupfox-config.nix WIP: accumulated changes 2026-05-25 16:24:21 -05:00
flake.lock Expand ene-rds Rust workspace and refine devcontainer 2026-05-19 07:52:39 +00:00
flake.nix chore(root): refresh package lock and flake outputs 2026-05-20 18:43:13 -05:00
GEMINI.md WIP: accumulated changes 2026-05-25 16:24:21 -05:00
GETTING_STARTED.md Refactor provenance sources for open witness backends 2026-05-12 05:57:04 -05:00
kilo.jsonc WIP: accumulated changes 2026-05-25 16:24:21 -05:00
LICENSE initial: sovereign research stack (consolidated, weightless, and lfs-optimized) 2026-05-04 18:11:36 -05:00
Modelfile integrate infrastructure config, axiom cleanup, and documentation updates 2026-05-17 12:03:19 -05:00
NOTICE Track HCMMR sources and ignore generated mirrors 2026-05-11 21:53:32 -05:00
opencode.json feat(pist): pist_trace_classify MCP tool — classify proof traces against 57-theorem flexure library 2026-05-26 11:23:53 -05:00
package-lock.json Bump better-sqlite3 in the root-npm-minor-patch group across 1 directory 2026-05-20 23:03:34 -05:00
package.json Bump better-sqlite3 in the root-npm-minor-patch group across 1 directory 2026-05-20 23:03:34 -05:00
pyrightconfig.json wip: refined investigation script for Erdős–Gyárfás conjecture 2026-05-08 14:50:03 -05:00
README.md docs: full documentation + roadmap refresh (2026-05-19) 2026-05-19 09:12:16 +00:00
requirements-optional-science.txt Add optional science toolbelt probe 2026-05-12 00:21:34 -05:00
result-devcontainer Expand devcontainer with full Python stack, add MCP servers (Notion/AWS), strengthen Lean theorems 2026-05-19 01:52:14 -05:00
run-container.sh integrate stashed changes: math model data updates + 4 receipt dirs + container config 2026-05-17 12:03:19 -05:00
system-packages-optional-science.txt Harden optional science toolbelt probe 2026-05-12 05:12:46 -05:00
THIRD_PARTY_NOTICES.md collapse: prover orchestration layers, FAMM verilator harness, swarm topological prober, spec sheets, virtual FPGA system tests, merge conflict resolution 2026-05-06 23:42:01 -05:00
TODO_MAP.md docs(agents): project-wide AGENTS.md audit — cross-refs, baseline, contracts 2026-05-26 22:34:46 -05:00

Research-Stack (OTOM)

Heretical Science Engineering

Ultra-low power, zero-decimal data routing and compression.

If you just stumbled across this repository, you might see words like "Topological State Machine" and "Manifold Points" and assume this is dense, academic magic. It isn't.

This project is actually built on a very simple, grounded idea: Modern computing is incredibly wasteful.

Right now, running AI or compressing massive datasets requires giant, power-hungry GPUs because they rely on Floating-Point Math (heavy decimals like 3.14159...). We prove that you don't need decimals. You can map complex data (like the grammar of the English language) into structural shapes, and navigate them using only simple integers (whole numbers).

Because we only use addition, subtraction, multiplication, and modulo, this system can run on a $15 blank-slate microchip (an FPGA) instead of a massive server farm.

🛠️ How we know it works (Zero Guesswork)

We do not guess that our integer math works. We prove it. The core of this project is written in Lean 4, a strict mathematical theorem prover. If our logic has a flaw, the code physically will not compile. We currently have 746 verified Lean modules across a 3,529-job deterministic build (0 errors) securing this engine.

Python, Rust, and Verilog only exist in this repository to act as "dumb pipes" to feed data into our proven mathematical core.


📁 Repository Structure (By Goal)

Everything is numbered so you know exactly what depends on what.

Folder What it actually is (Plain English)
0-Core-Formalism/ The Brain. Lean 4 code. The mathematically proven integer arithmetic. This is the source of truth.
1-Distributed-Systems/ The Network. Code for making multiple computers talk to each other to share the workload.
2-Search-Space/ The Navigator. Algorithms that search through our data shapes to find the best routes.
3-Mathematical-Models/ The Library. Where we store our databases of equations and compressed English grammar shapes.
4-Infrastructure/ The Drivers. Code that physically talks to the hardware, GPUs, and APIs.
5-Applications/ The Executables. Python scripts that run the system end-to-end. (These are just shims connecting data to our Lean 4 Brain).
6-Documentation/ The Manual. Where you'll find plain-English explanations and our theoretical papers.
shared-data/ Raw data, cache, and exported files.

📖 Where to start?

If you are new here, read these two files first:

  1. Explanation for Humans - A translation guide for our technical jargon.
  2. Calculator-Plain Math - Proof that every complex concept we use can be calculated on a high-school graphing calculator.

🚀 Quick Start

# 1. Compile the mathematically proven core (Takes ~1-2 minutes)
cd "0-Core-Formalism/lean/Semantics"
lake build

# 2. Run the English Manifold Builder (Compresses English via grammar shapes)
cd "../../.."
python3 5-Applications/scripts/redpajama_english_manifold.py

⚖️ The One Rule for Contributors

Lean is the source of truth. If you add logic, it goes in 0-Core-Formalism/lean/Semantics/ and must be mathematically proven. Python scripts may not contain complex math, branching logic, or cost functions. Python is just the delivery boy for Lean.


🗄️ Infrastructure (Current)

Component Description
4-Infrastructure/infra/ene-rds/ Rust workspace (8 crates) replacing the Python RDS stack — Axum HTTP API, PostgreSQL, Ollama embeddings
4-Infrastructure/storage/ restic + Garage S3 (v2.3.0, Tailscale mesh) + rclone storage stack with automated observer agent
.devcontainer/ NixOS hermetic devcontainer with OpenGL/X11, Lean, Python science stack, MCP servers (Notion + AWS)
4-Infrastructure/infra/credential_server.py Credential gateway with apiProvider service kind and cupfox routing

Research Stack — All Rights Reserved