# Overview: what this project checks, proves and corrects This is a standalone explanation that can be shared with people who have not seen the rest of the project. It covers the whole body of work, not only the most recent change. ## 1. What the project is The source material is a set of research documents: three theses (`THESIS.md`, `THESIS (1).md`, `THESIS (2).md`, `THESIS2.md`), an interactive explorer (`prime-circle-math.html`), *Lattice vs Abacus*, and two volumes of the *Codex* (PDFs). Together they argue that ancient counting systems (the 360° dial, base 60, the 19×19 board, the flower of life, the abacus, the circle of fifths, kissing spheres) were deliberately engineered around primes and modular arithmetic, and they propose using that structure for exact computation (π, square roots, rotation, rendering). The project turns every exact mathematical claim in that material into a statement in the Lean proof assistant and either proves it, disproves it, or corrects it. **Everything described as "proved" below is machine-checked**: the full project (37 Lean files in `RequestProject/`, about 425 theorems and lemmas) builds with no `sorry` (no unfinished proofs) and uses only Lean's standard axioms. A few finite enumerations use compiled evaluation (`native_decide`); these are marked **(nd)**. ## 2. Where to read more | File | Contents | |---|---| | `SYNTHESIS.md` | The main write-up: how all proved results fit into one structure, with theorem names | | `AUDIT.md` | Claim-by-claim audit of the source documents: proved / false / imprecise / empirical / not formalized | | `SHARED_MODEL.md` | Map from the documents' terminology to standard mathematical structures | | `RENDERING_AUDIT.md` | Square-root tables, vector arithmetic, the folded clock, rendering and projection | | `SELF_SIMILAR_MODEL.md` | The recursive "cell" (centre, shell, rods, copying, rescaling) across all figures | | `RECURSIVE_REASSESSMENT.md` | The φ-depth ("count the open spokes") recursion and why 360 and 361 both take seven steps | | `bench/` | A single-machine C benchmark (not formally verified) | ## 3. The main proved results ### Why the classical bases are what they are (`Synthesis.lean`) Each base is the **smallest** number with its divisibility property, and exactly its multiples have that property: - **12**: smallest count that splits into halves, thirds and quarters (`twelve_design`). - **60**: smallest count divisible by every number 1–6 (`sixty_design`). - **360**: smallest dial divisible by every number 1–10 except 7 (`three_sixty_design`). - **2520 = 360 × 7**: smallest count divisible by every number 1–10 (`twenty_five_twenty_design`). ### The dial (360 and 7) - A dial of size `N` has a `k`-fold turn exactly when `k` divides `N`. - For a prime step `q`: `q` visits every position ⇔ `q` does not divide `N` ⇔ the dial has no `q`-fold turn (`step_walks_iff_no_rotation`). So **7 is the smallest step that walks the whole 360 dial** and also walks the 12-note circle of fifths (`seven_least_generator`). - `n² ≡ 1 (mod 360)` exactly when `n ≡ 1, 19, 71, 89 (mod 90)`; 19 is the smallest such `n > 1`. - φ(360) = 96 open spokes. Below 5,000,000 every open spoke holds between 3,572 and 3,685 primes, about a 3% spread (`primes_evenly_spread`, nd). - Schatunowsky's theorem is proved in full. As a consequence the rule "a prime reduced mod 360 lands on a prime spoke" holds below 409 and first fails at 409, which lands on 49. ### Two lattices and the class of a prime mod 12 - The square grid (`x² + y²`) splits at an odd prime `p` exactly when `p ≡ 1 (mod 4)`; the flower/hexagonal lattice (`x² − xy + y²`) splits exactly when `p ≡ 1 (mod 3)`. In both cases, splitting means the lattice's own rotation fits on the dial mod `p`. - For primes `p ≥ 5`, the remainder mod 12 decides both lattices at once, with all four combinations occurring (`two_lattice_fingerprint`). **7 and 19 are in the same class** (remainder 7): flower-splitting, grid-inert. - A prime `p ≡ 1 (mod 4)` is a sum of two squares in exactly one way, so the circle `x² + y² = p` meets the grid in exactly 8 points; for `p ≡ 3 (mod 4)` (e.g. 19) it meets none. ### The 19×19 board is a number system with 360 as its dial - Read mod 19, the board is a field with 361 elements. Its 360 non-centre crossings form a single cycle generated by `1 + 3i`; 90 steps is the quarter turn; the codex's `1 + 9√2` also generates the cycle and has order 360; 96 elements generate it. - 19 is the only `n` with `n² − 1 = 360` (`sq_sub_one_eq_360_iff`). The same centre-removal pattern appears as `9² − 3² = 72`. - By contrast, the 96 open spokes of the bare 360 dial do not form a single cycle (their largest order is 12). ### Rods (the Chinese remainder theorem) - Arithmetic mod 360 is three independent rods mod 8, 9, 5 (mod 144000: 128, 9, 125), with no carries between rods. 19² lands on (1, 1, 1). - TAB VII's 72 dots split exactly into an 8-wheel and a 9-wheel, and 5 · 72 = 360. ### Exact scaling and depth - **Base 60** is closed under +, −, ×; division by `n` is exact iff `n` has no prime factors other than 2, 3, 5. Extending the depth never changes digits already computed. π = 3;8,29,44,0,47…, and three polygon doublings give one more base-60 place. - **Precision is known in advance**: if radii are at most `60^m` and π is known to `k + m` base-60 places, every side `s = r√π` is correct to `k` places (`side_precision`). A table of prime square roots with relative error ε gives any `√n` with error at most `(1+ε)^k − 1`. - **Flower of life**: the seed of life (centre + 6) is a complete digit set; every lattice point has exactly one address at every depth; each level is the previous one scaled by `√7`; a depth-7 super-cell holds 7⁷ = 823,543 cells; the ring totals are the cubes `n³`. - **Dimensions**: ball volumes satisfy `V_{n+2} = (2πr²/(n+2))·V_n` exactly; the Gaussian integral over n dimensions is `(√π)ⁿ`; one kissing arrangement works in every dimension with `2n(n−1)` contacts. - **φ-depth** (Shapiro's law, machine-checked): the number of "count the open spokes" steps to 1 is given by an additive weight, which explains why 360 and 361 both take exactly seven steps, and bounds depth between base-2 and base-3 logarithms. ### The continuum and the proved limits - √π is irrational; the golden ratio enters through `2cos 72°`; no lattice has a 5-fold turn; twelve fifths never equal seven octaves (the Pythagorean comma is about 23.46 cents). - Proved limits: no single encoding turns both + and × into vector addition (and zero cannot be included); no continuous square root on the circle; the perspective divide is not affine; uniform scaling of a scene saves no rendering work; the unit ball fills a vanishing fraction of its bounding box as dimension grows. - Supported for computation: drift-free rotation by integer dial indices, carry-free rod arithmetic, precomputed prime-root tables with known error budgets, exact base-60 fixed point for 2-, 3-, 5-smooth divisors. ## 4. What was found wrong or imprecise in the source documents 1. Inverse derivative: only true for `x > 0`; for `x < 0` the product is −1. 2. "Kissing" gap: it is negative, so those circles overlap rather than touch. 3. Descartes/Soddy formula: the quoted form is the special case where one circle is a straight line (now proved as geometry for that case). 4. 19 and the layers: "`p − 1` divides every layer" holds for 22 primes, not only 19; 19² is not ≡ 1 modulo any layer. 5. "Highly composite": none of the temporal layers (including 144000) is highly composite; they are 5-smooth. 6. Codex Folio VIII: the board's corners are crossings, and the corner products are ±81, not ±361. 7. C code in `THESIS2.md`: `geom_sqrt` and `radius_from_area` call each other with no base case; `r = √(A/π)` itself needs a square root. 8. `THESIS (2).md` lists "structured boundary effects" as proven, but gives no precise statement. ## 5. What is not established - **Speed claims**: only a single-machine benchmark exists (`bench/`). Precomputed camera trigonometry was about 13% faster at 100 vertices and about 1% at 10,000; per-object table lookup was about 2.3–3.3× faster; float matrices drifted while dial indices returned exactly to 0. None of this is formally verified. - **Empirical scores** in the documents: no data was supplied, so they are unchecked. - **Known theorems not formalized here**: hairy ball theorem, Lindemann (π transcendental), torus-knot invariants, the icosahedral group being A₅, Gauss–Wantzel. (The general four-circle Descartes theorem and five-sphere Soddy theorem were proved later, in `RequestProject/DescartesGeneral.lean`.) - **Open next steps**: a precise definition of a "depth-7 hyper-dimensional object" if one specific object is intended. (The general flower statement — every prime `p ≡ 1 (mod 3)` is `x² − xy + y²` — and the single rods theorem for turn orders were proved later, in `RequestProject/FlowerPrimes.lean` and `RequestProject/RodOrders.lean`.) - **Historical intent**: the proofs show what each ancient choice achieves and that several are optimal; that the builders chose them knowingly rests on the textual sources, which a proof cannot date. - **Rods principle (later):** `RODS_PRINCIPLE.md` develops the turn-order rods theorem, its consequences and a four-pass re-examination of every earlier verdict (corner products and the "unreachable corner" are recoverable once read as the text intends; 7200 and 14400 are divisor records among regular numbers; 19 is the least "two-spoke" prime). - **The seventh bin (later):** `SEVENTH_RIM.md` re-examines the revised outer bound `7 × 144000 = 1008000` in seven passes: `864000` becomes the working cycle, the rim is the first multiple of the base divisible by every digit 1–10, the admissible primes grow from 35 to 71 (the new 36 are exactly those with `7 | p − 1`), `71` plays the role of `19` for the heptad-closed dial `2520`, and `1008001` is prime.