df4d2309e9
- 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
5.4 KiB
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.