Blog
I checked my own eight theorems by machine. Four held, three headings were wrong
Every proof verified step by step, every verdict attacked by a second pass, none disputed — and the defects were never in a measurement, always in what a heading claimed about it.
- EIGHT THEOREMSFour held as standard results.
- THE MACHINETwo passes disputed no verdicts.
- THE HEADINGSThree headings overstated their results.
The proofs page carried eight theorems. I had written them and never checked them mechanically. So: each one verified by computation, and each verdict then attacked by a second independent pass trying to show the label was too generous or too harsh.
Zero verdicts were disputed. Here is what came back.
Four held
| statement | label | |
|---|---|---|
| 1 | phi² + 1/phi² = 3 | [Verified] |
| 2 | optimal integer radix is 3 | [Verified] |
| 3 | log₂(3) bits per trit | [Verified] |
| 5 | F(n+1)/F(n) → phi | [Verified] |
And all four are textbook. Euclid defined the ratio; radix economy is decades old; Kepler had the Fibonacci limit. Citing them correctly is not a loss — a paper that sources its results is stronger than one that appears to have derived everything.
One was false as stated
Theorem 4 said ternary binding is its own inverse: unbind(bind(a,b),b) = a. Its own Step 1 defines binding as integer multiplication on {-1,0,+1}, and under exactly that definition zero is an annihilator — 0 × a = 0 for every a, and nothing recovers a from it.
It fails in 2 of 9 per-position cases and in every vector trial at every dimension tested. Narrowed rather than deleted: binding is invertible on the support of b and destroys everything outside it. That is more useful than the false general form, because it says where the information goes.
Two headings claimed more than the work
Theorem 7 claimed uniqueness of an ansatz. Uniqueness is the strongest word available and the claim never states the domain it is unique over — "all forms with at most five free parameters" is uncountable if the parameters are real, so no search establishes it there. Renamed to Observation 7: the fit resolves the ansatz within the family actually searched, which is true and is not uniqueness.
Theorem 8 proves what Theorem 2 proves. Two headings for one result overstate how much is established. Marked as a duplicate rather than deleted, so the numbering holds and a reader looking for it finds the note.
And one is a coincidence worth stating as one
Theorem 6: dim(E8) = 3⁵ + 5 = 248. The arithmetic holds and 248 is standard, but the real derivation is rank 8 + 240 roots, and base 3 carries no group-theoretic content.
What makes it worth keeping is the search: 248 = bᵉ + k has exactly one solution for b ≤ 16, e in 2..8, k ≤ 20. Widening the net fourfold produced no second. That is a real, cheap, falsifiable statement — and a rare coincidence is still not a mechanism. Labelled [Empirical fit] with the search space stated.
The pattern
Not one defect was in a measurement. Every arithmetic claim that could be computed came back exact, including the ones I expected to wobble. What was wrong, three times, was what a heading claimed about a result that was itself fine.
A theorem needs a derivation connecting its terms. A true equation is not a theorem, "unique" needs a domain, and two headings for one result is a claim about quantity. All three are free to fix and none of them costs a number.
What this does not settle
- The audit was run 2026-08-11. The theorems themselves date from the proofs page as it stood before that; the corrections are dated in place there.
- The audit checked arithmetic, derivation and prior art. It did not check whether the theorems are useful, and a correct standard result cited correctly can still be the wrong thing to build on.
- Theorem 6’s isolation search covered b <= 16, e in 2..8, k <= 20. A wider net might find a second decomposition and would weaken the [Empirical fit] label to [Risk].
- Observation 7 still has no stated domain. Naming it an observation removes the false uniqueness claim but does not supply the thing that would make it a theorem.
Receipts
Work with me
Want this kind of check on your own design?
I audit RTL and build independent, bit-exact models, then take the result through synthesis and, when useful, onto an Artix-7 board. The first conformance module is free.