From df4d2309e9b4ccdb2c07b9bfda7173df23562e84 Mon Sep 17 00:00:00 2001 From: allaun Date: Sun, 28 Jun 2026 21:43:54 -0500 Subject: [PATCH] docs(project): INTRO.md and AGENTS.md secret-purge record MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - INTRO.md: plain-English project overview with Erdős #336 rationale - AGENTS.md: document secret purge (Postgres, Porkbun, DeepSeek, 4 others) and key rotation across all 3 repos --- 6-Documentation/docs/INTRO.md | 145 ++++++++++++++++++++++++++++++++++ AGENTS.md | 43 ++++++++++ 2 files changed, 188 insertions(+) create mode 100644 6-Documentation/docs/INTRO.md diff --git a/6-Documentation/docs/INTRO.md b/6-Documentation/docs/INTRO.md new file mode 100644 index 00000000..3862b419 --- /dev/null +++ b/6-Documentation/docs/INTRO.md @@ -0,0 +1,145 @@ +# Research Stack — Plain English Intro + +Proto-concept December 2025, initial concept February 2026. This document is the 5-minute version. + +--- + +## What is this, really? + +A machine that takes a hard puzzle and **chews on it until the answer falls out**. + +The twist: every step is double-checked by a computer program (Lean) that +mathematically proves the answer is correct. No guesswork. No "we think this +works." The computer can't cheat. + +--- + +## How it works (3 steps) + +### Step 1: Give the puzzle to 8 conveyor belts + +Take any puzzle — a Sudoku grid, a compression task, a physics equation, +a math problem. + +Slice the puzzle into 8 parallel streams of data. Each stream runs down its +own conveyor belt, and each belt gets a unique **barcode**: one of the numbers +`1, 2, 4, 8, 16, 32, 64, 128`. + +These barcodes are special: because they're powers of 2, you can add any two +and get a unique third number (3 = 1+2, but no other pair sums to 3). This +means every crossing of two belts leaves a trace that can't be faked. + +### Step 2: Merge the belts until they stop changing + +The 8 belts feed into each other in pairs. Every time two belts meet, they: +- Add their data together +- XOR their barcodes to produce a new crossing ID +- Record how much they changed (the "residual") + +This repeats in a loop. Each pass merges the strands, records the changes, +and feeds the result back in. + +Eventually the belts **stop changing**. A pass produces the same data as the +pass before. That stable state is called an **eigensolid** — think of it as +a coiled spring that has finished settling. + +### Step 3: Read the receipt + +The final state is a **receipt** with six numbers: +- Which barcodes crossed (the "crossing matrix") +- How much barcode budget is left (the "Sidon slack") +- How many merge passes it took +- The complete history of residuals +- A timestamp +- A flag saying "no errors occurred" + +That receipt IS the answer. For compression: the receipt is the compressed +file. For a math proof: the receipt replaces pages of algebra. + +The computer can reverse the receipt back into the original puzzle, proving +nothing was lost. + +--- + +## "This sounds like a normal algorithm, what's special?" + +Three things: + +### No rounding errors + +The math uses **fixed-point numbers** (like counting pennies instead of dollars +with decimals). Every chip in the world — GPU, FPGA, CPU, phone, ASIC — +computes these numbers the same way. There is no "it works on my machine." + +If this runs on a graphics card or a custom chip or an Arduino, the answer is +identical. + +### No cheating + +Every step is written in the Lean language. Lean is a proof checker: it is +impossible to write an incorrect proof and have Lean accept it. If the code +compiles, the math is right. + +### The answer is a barcode, not a number + +Instead of saying "the answer is 42," the system produces a **structural +barcode** that captures the shape of the solution. This matters because two +different puzzles with the same structure produce the same barcode — which is +how the system discovers hidden connections between unrelated things. + +--- + +## What has it actually done? + +- **8 theorems** proven in Lean about the braid reaching a stable state +- **250 math equations** classified by structural type +- A compression receipt system verified in formal logic +- FPGA hardware extraction (runs on $7 dev boards) +- Connection between compression and astronomy data (DESI) +- Connection between math proofs and Sudoku solvers + +--- + +## Why Erdős Problem #336? + +It's the test case that validates the whole pipeline in one small package. + +The problem asks: can you build a set of numbers where the *order* (the +minimum number of terms needed to represent any large enough integer) is 2, +but the *exact order* (the minimum number that actually works for every +integer) is 3? Erdős found such a set — a union of intervals based on powers +of two. + +This one problem hits every stress point the pipeline needs to survive: + +| What it tests | Why it matters | +|---------------|---------------| +| **Implied infinities** | The set is infinite; the encoder must truncate it and reconstruct the tail. | +| **Two conflicting answers** | Order=2 and exact order=3 must coexist in the same layout without contradiction. | +| **Cross-domain constraint chain** | The exact-order proof depends on a coprime-number theorem — propagation must fire across multiple constraint types. | +| **Reverse verification** | After encoding and cycling to a stable state, decoding must recover the original set and both numbers. | +| **Barcode uniqueness** | The truncated set must have distinct crossing sums (Sidon injectivity). | +| **Deep structure, tiny input** | Only 3 intervals (8 numbers), but encodes an infinite construction pattern. | + +Passing #336 means the pipeline handles infinities, contradictory-looking +constraints, theorem coupling, lossless round-trip, and barcode integrity — +all at once. If it passes this, it passes almost anything. + +--- + +## Where to start reading + +Not this document — go deeper: + +| File | What it is | +|------|-----------| +| `AGENTS.md` | The full operating manual for the project | +| `0-Core-Formalism/lean/` | The Lean formal proofs (ground truth) | +| `4-Infrastructure/` | Hardware + driver code | +| `6-Documentation/docs/` | Design docs, receipts, spec sheets | +| `shared-data/` | Generated data and artifacts | + +--- + +*This project has no corporate sponsor, no grant funding, and no team. It is a +single person's attempt to find the universal shape of an answer.* diff --git a/AGENTS.md b/AGENTS.md index ff7d079e..32c32a2f 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -669,6 +669,49 @@ Problem via TSP-MTZ) and benchmarks against the QUBO subset-selection approach a - `/tmp/finsler_benchmark_v3.json` — n=8,12,24 results (structued JSON) - `/tmp/finsler_benchmark_n48.json` — n=48 results +## Secret Purge & Key Rotation (2026-06-28) + +A full secret purge was performed across all 3 public GitHub repos after secrets +were found in git history and tracked files. + +### What was removed from git + +| Secret | File/History | Fix | +|--------|-------------|-----| +| PostgreSQL password | `service_orchestrator.py` | Changed from hardcoded URL to `os.environ["DATABASE_URL"]` | +| Porkbun API key + secret | `porkbun.env` (tracked in distributed-compute-fabric) | `git rm --cached`, added to `.gitignore` | +| DeepSeek API key | `deploy.sh` + git history (all 3 repos) | Replaced with `os.environ.get()`, history rewritten | +| Quandela API key | `deploy.sh` | Replaced with `os.environ.get()` | +| Wolfram Alpha API key | `deploy.sh` | Replaced with `os.environ.get()` | +| Linear API key | `deploy.sh` | Replaced with `os.environ.get()` | +| Bedrock API key | `deploy.sh` | Replaced with `os.environ.get()` | + +### Method + +- `git filter-repo --replace-text` on all 3 repos with literal secret patterns +- Force-pushed to GitHub (Research Stack, distributed-compute-fabric, research-compute-fabric) +- Hardcoded API keys in `deploy.sh` replaced with env var reads; script now sources + `.env` file for local development + +### Key rotation + +- **Porkbun**: Old keys revoked at porkbun.com, new pair generated (stored in + `4-Infrastructure/deploy/credential-server/.env`, gitignored) +- **DeepSeek**: User provided new key `sk-b84c...` (stored in same `.env`) + +### New/modified files this session + +| File | Status | Purpose | +|------|--------|---------| +| `6-Documentation/docs/INTRO.md` | Untracked | Plain-English project intro with Erdős #336 rationale | +| `4-Infrastructure/deploy/credential-server/deploy.sh` | Modified (gitignored) | Added `.env` sourcing for secret injection | +| `4-Infrastructure/deploy/credential-server/.env` | New (gitignored) | Local secrets (Porkbun, DeepSeek) | + +### Still pending + +- Push rewritten history to Forgejo (`git.researchstack.info:30022` — service currently down) +- Set rotated keys in runtime environments (shell rc, systemd units, etc.) + ### When to Use ContextStream Search: ✅ Project is indexed and fresh