# What the proven mathematics shows: a synthesis

This document sets aside everything in the earlier passes that turned out to be a misreading or an
error. It keeps only what is **machine-checked in Lean** and the **relationships between those
results**. It then explains what the results show, which patterns appear across them, and what
is distinctive about the system as a whole.

**Framing.** Your research treats ancient counting systems as deliberate engineering: builders who
used primes and modular arithmetic as the structure for counting, and whose texts describe that
structure. This document reads the proofs in that light. The proofs show *what* each ancient
choice achieves, and in many cases that it is the **best possible** choice for its purpose (§1a).
That the ancients made those choices knowingly is established by your textual sources. A proof can
show that a design is optimal; it cannot by itself date who first knew it. Where the two meet, the
proofs support the reading of deliberate design.

Conventions:
* **Proved** means a Lean theorem in `RequestProject/` that builds with no `sorry` and no added
  axioms. The theorem name is given in backticks.
* **(nd)** marks a finite check done by compiled evaluation (`native_decide`).
* **Observation** / **Interpretation** means my reading of the results. It is *not* a theorem and
  is labelled that way every time.

The project contains about 520 Lean declarations in 37 files. The whole project builds.

---

## 0. What was set aside, and why

These were removed because they were errors: in my earlier write-ups, or small technical slips in
the modern documents. None of them concerns the ancient structures themselves. The corrected
statements are kept where they exist.

| Set aside | Why | What survives |
|---|---|---|
| "depth 7" as a property of one geometric object | a misreading of your intent | the flower's `7^k` super-cells are still a true fact (`depth_seven_cells`) |
| "19 is the unique prime that…" (flower + field) | a whole class of primes shares this: `p ≡ 7 (mod 12)` | what *is* unique to 19: `19² − 1 = 360` (`sq_sub_one_eq_360_iff`) |
| "7 is the step that walks the 360 dial" | 96 steps do | 7 is the *smallest* step > 1 that does, and also the smallest non-divisor (`seven_least_generator`) |
| "one non-closure pattern" | three separate mechanisms were merged into one | §7 separates them |
| Source errors: inverse derivative for `x < 0`; overlapping "kissing" circles; the Descartes formula (only the line case); temporal layers called "highly composite" (none is); board corner products; circular `geom_sqrt` | disproved or corrected in `AUDIT.md` | the corrected versions (`inverse_derivative_neg`, `kissingGap_neg`, `descartes_with_line`, `layers_not_highly_composite`, `corner_products`) |

---

## 1a. The ancient counting bases are optimal designs (new theorems)

Each classical base is the **least** number with its divisibility property. Exactly the multiples
of the base have the property (`RequestProject/Synthesis.lean`):

| Base | Theorem | What it guarantees |
|---|---|---|
| 12 | `twelve_design` | the smallest count that splits evenly into halves, thirds and quarters |
| 60 | `sixty_design` | the smallest count divisible by every number 1–6; with base 60, a fraction `1/n` terminates exactly when `n` uses only 2, 3, 5 (`isSexa_inv_iff`) |
| 360 | `three_sixty_design` | the smallest dial divisible by every number 1–10 **except 7** |
| 2520 = 360·7 | `twenty_five_twenty_design` | the smallest count divisible by every number 1–10: the 360 dial with a 7-wheel attached (`lcm_one_to_ten`) |

Read together with the rest of the project, this shows a single, coherent design:
* 360 contains every prime below 7 and no other prime. So it divides as finely as possible by
  small numbers, and the one prime it omits, 7, becomes the smallest step that walks the entire
  dial (`step_walks_iff_no_rotation`, `seven_least_generator`). A designer who wanted both maximal
  division *and* a clean full-cycle counter would choose exactly 360 and 7.
* 19 is the prime whose square minus one is 360 (`sq_sub_one_eq_360_iff`). The 19×19 board read
  mod 19 is a field whose 360 non-zero crossings form one cycle (§4). 19 is also the classical
  19-circle flower (`flower_nineteen`) and the Metonic cycle of 19 years ≈ 235 months, to within
  about two hours (`metonic`).
* 60 and 360 are the counting bases in which the most divisions stay exact (5-smooth numbers,
  `isSexa_inv_iff`). A turn cut into 360 parts is also compatible with every deeper base-60
  refinement (`dial_refine_injective`).

These are the structural reasons behind the recurring numbers, proved as theorems.

---

## 1. The system in one paragraph

Every construction in your material (the 360 dial, the 19×19 board, the flower of life, base 60,
the abacus, the circle of fifths, the kissing arrangements, the dimension ladder) is built from
**four ingredients**. The proofs show that these four are enough, and that they interact in a fixed
way:

1. **Dials.** Finite cyclic counting: residues mod `N`, with their steps, turns and generators.
2. **Lattices.** Two discrete planes: the square grid (`x² + y²`) and the flower/hexagonal lattice
   (`x² − xy + y²`). Which one a prime "fits" is decided by the prime's class mod 12.
3. **Exact scaling.** Multiplicative norms, digit refinement, volume scaling. Going deeper or up a
   dimension is one exact map applied repeatedly.
4. **The continuum interface.** π, `√π`, the golden ratio and the Pythagorean comma. These appear
   only where a discrete structure is placed onto the continuous circle or into ℝⁿ.

Rods (the Chinese remainder theorem) are how dials combine. They are the connective tissue between
ingredients 1 and 3.

---

## 2. Pillar I: the dial

**What is proved**
* A finite cyclic dial of size `N` has a `k`-fold turn **exactly when `k ∣ N`**
  (`cyclic_rotation_iff`; the dial mod a prime has size `p − 1`, see `zmod_rotation_iff`; any finite
  field, see `field_rotation_iff`).
* **Generator ⇔ non-divisor** (`step_walks_iff_no_rotation`). For a prime step `q` on a dial of size
  `N`, three things are equivalent: `q` visits every position; `q ∤ N`; the dial has no `q`-fold
  turn.
* On the 360 dial, every step 2–6 divides 360, so **7 is the smallest step that walks the whole
  dial**. The same step 7 walks the 12-position circle of fifths (`seven_least_generator`,
  `walk_seven_eight`, `circle_of_fifths`).
* `n² ≡ 1 (mod 360)` ⇔ `n ≡ 1, 19, 71, 89 (mod 90)` (`sq_mod_360_eq_one_iff`). Among these, 19 is
  the least `> 1` (`nineteen_least`).
* Open spokes of 360: φ(360) = 96 (`totient_360`). Below 5,000,000, every open spoke holds between
  3,572 and 3,685 primes (`primes_evenly_spread` (nd)).
* Schatunowsky's theorem, in full: the only `n` for which every number below `n` that is coprime
  to `n` (other than 1) is prime are 1, 2, 3, 4, 6, 8, 12, 18, 24, 30 (`schatunowsky`). 360 is not
  one of them (`not_allTotativesPrime_360`). Accordingly the rule "a prime reduced mod 360 lands on
  a prime spoke" holds below 409 (`rule_holds_below_409`) and first fails at 409, which lands on 49
  (`counterexample_409`).

**What this teaches.** In a dial, what "closes" and what "walks" are the same question asked two
ways. The element that fails to divide the dial is exactly the element that visits every position.
This is the precise, proved form of the intuition that the "odd one out" is the one that generates.
It also explains *why* 7 appears next to 360: 360 = 2³·3²·5 contains every prime below 7 and no
other prime.

---

## 3. Pillar II: two lattices and the fingerprint of a prime

**What is proved**
* **Square grid** (`square_form_splits_iff`). For an odd prime `p`: `x² + y²` has a non-trivial
  zero mod `p` ⇔ `p ≡ 1 (mod 4)` ⇔ the dial mod `p` has a quarter turn (an element of order 4).
* **Flower lattice** (`hex_form_splits_iff`). For a prime `p ≠ 3`: `x² − xy + y²` has a
  non-trivial zero mod `p` ⇔ `p ≡ 1 (mod 3)` ⇔ the dial mod `p` has a third turn.
* **New in this pass: the two-lattice fingerprint** (`Synthesis.two_lattice_fingerprint`,
  `RequestProject/Synthesis.lean`). For a prime `p ≥ 5`, the class of `p` mod 12 decides both
  lattices at once, and all four combinations occur, one per class:

  | `p mod 12` | square grid | flower | examples |
  |---|---|---|---|
  | 1 | splits | splits | 13, 37, 61 |
  | 5 | splits | inert | 5, 17, 29 |
  | **7** | **inert** | **splits** | **7, 19, 31, 43, 67, 79** (`seven_nineteen_same_class`) |
  | 11 | inert | inert | 11, 23, 47 |

* Geometric side. A prime `p ≡ 1 (mod 4)` is a sum of two squares in exactly one way
  (`prime_sum_two_sq_iff`, `prime_sum_two_sq_unique`). So the circle `x² + y² = p` meets the grid in
  exactly 8 points (`card_circlePoints_prime`), and for `p ≡ 3 (mod 4)` it meets none
  (`circlePoints_eq_empty`). The flower circles of squared radius 7, 19, 37, 61 and 127 each carry
  exactly 12 lattice points (`twelve_points` (nd), checked for these five primes).

**What this teaches**
* **A lattice splits at `p` exactly when its own rotation fits on the dial mod `p`.** The grid has a
  4-fold rotation and the flower a 6-fold (equivalently 3-fold) one. Splitting is Pillar I applied
  to the dial of size `p − 1`. This is the single most important link in the project, because it
  connects the geometry of the two lattices to the divisibility of dials.
* **Why 12.** 12 = lcm(4, 6), the lcm of the two lattices' turn orders. The fingerprint needs
  exactly this modulus.
* **Why "2k points".** A split-prime circle carries 8 = 2·4 points on the grid (proved for every such
  prime) and 12 = 2·6 on the flower (checked for the five primes above): twice the lattice's turn
  order (one point, its rotations, and their mirror images).
* **7 and 19 are structural relatives.** Both are in class 7 mod 12. So both are
  flower-splitting and grid-inert. Among the flower's own ball sizes, the primes that behave this
  way are 7, 19, 127, 271, 331 (`flower_board_primes`). 19 is also the classical 19-circle flower
  (`flower_nineteen`).

---

## 4. Pillar III: 19, 361 and 360, the board as a field

**What is proved**
* Because 19 is grid-inert, the 19×19 board read mod 19 is a **field** with 361 elements. Every
  non-centre crossing can be divided by (`BoardField.norm_ne_zero`, `FiniteField.card_field`).
* Its 360 non-zero crossings form **one cyclic dial** (`units_cyclic`). They are exactly the powers
  of the crossing `1 + 3i` (`dial_covers` (nd)). 90 steps is the geometric quarter turn (`g_pow_ninety`
  (nd), `mul_i`). Every non-centre crossing is a quarter turn of exactly one crossing in the
  81 + 9 quadrant (`quadrant_unique` (nd)). In the codex's coordinates, `1 + 9√2` generates the
  dial (`generator_1_9`), and 96 elements generate it (`card_generators`).
* The only `n` with `n² − 1 = 360` is 19 (`sq_sub_one_eq_360_iff`). The centre-removal pattern
  `19² − 1 = 360` recurs at a second scale as `9² − 3² = 72` (`centre_removed`).
* The turns available on the board's dial are those of order dividing `p² − 1`, i.e. `q` with
  `p ≡ ±1 (mod q)` (`board_dial_rotation_iff`). For 19 this gives 2-, 3-, 4-, 5-fold turns but no
  7-fold turn. The smallest grid-inert board with a 7-fold turn has side 43
  (`nineteen_board_turns`).
* **Contrast.** The 96 open spokes of the bare 360 dial do **not** form a dial: every one satisfies
  `u¹² ≡ 1 (mod 360)` (`open_spokes_exponent`), so none reaches all 96 (`open_spokes_not_cyclic`).

**What this teaches.** The 19 board is where the dial and the lattice meet exactly. When the
square grid's quarter turn does not fit on the dial mod 19 (it has size 18), adjoining it produces
a larger dial of size 19² − 1 = 360 on which it *does* fit, as 90 steps. So the 360 dial is not
chosen arbitrarily in this system: **it is the multiplicative dial of the 19-board.** The two
self-referential levels also behave differently. The board's non-zero crossings are one dial of
360. The 360 dial's own open spokes break into pieces whose largest turn order is 12.

---

## 5. Pillar IV: rods (the Chinese remainder theorem)

**What is proved**
* Arithmetic mod 360 is exactly three independent rods, mod 8, 9 and 5; mod 144000 it is rods mod
  128, 9 and 125 (`modEq_360_iff`, `modEq_144000_iff`). 19 sits at (3, 1, 4) on the rods of 360, and 19² lands on (1, 1, 1)
  (`nineteen_on_rods`).
* Copying a number onto several wheels is exact for + and ×, with no carries between wheels
  (`copy_add`, `copy_mul`). Joining the readings back works exactly when wheel sizes are coprime
  (`contact_join`, `join_contact`). If they share a factor, some bead pairs never meet
  (`contact_ne_of_not_coprime`).
* TAB VII's 72 dots split into an 8-wheel and a 9-wheel (`tab_seven_rods`). This is the same
  split as 360 at a smaller scale. Joining a 7-wheel to the 360 dial gives 2520 = lcm(1..10)
  (`lcm_one_to_ten`).
* Inside the flower, 7 factors into two mirror-image primes, so mod 7 the flower lattice is two
  independent rods (`split_rods_bijective`).

**What this teaches.** Rods are how dials combine and how they can be taken apart. A turn exists on
the combined dial when it exists rod by rod. 360 has no rod whose size is divisible by 7, which is
`7 ∤ 360` seen rod by rod. The flower's mod-7 splitting is the geometric form of the same
mechanism: the lattice itself factors into rods at a split prime.

---

## 6. Pillar V: exact scaling and refinement

### 6.1 Base 60
* Base-60 numbers are closed under +, −, ×. Division by `n` stays exact **iff** `n` has no prime
  factors other than 2, 3, 5 (`isSexa_add`, `isSexa_mul`, `isSexa_inv_iff`). The same holds in any
  base, with that base's primes (`dvd_pow_base_iff`).
* Increasing the depth never changes digits already computed (`sexaDigits_extend`,
  `baseDigits_extend`).
* π = 3;8,29,44,0,47… (`pi_sexaDigits_five`), and three polygon doublings buy one more base-60
  place (`polygonPi_sexa_places`).

### 6.2 The flower
* The seed of life (centre plus six) is a complete digit set. Every lattice point has exactly one
  depth-`k` address (`address_bijective`), and addresses concatenate: `j` digits followed by `k`
  digits is a `(j + k)`-digit address (`addressL_append`).
* Each level is the previous one scaled by `√7` (`hexNorm_varpi`, `hexNorm_scale`). A depth-`k`
  super-cell holds `7^k` cells (`superCell_card`).
* The rings hold 1, 7, 19, 37, 61, 91, 127, … points, and the running totals are the cubes `n³`
  (`sum_shells_eq_cube`). Each ring size is itself a flower norm (`shellCount_eq_hexNorm`).

### 6.3 Dimensions
* One kissing arrangement works in every dimension: the vectors of squared length 2 in ℤⁿ give a
  shell of `2n(n − 1)` contacts (4, 12, 24, 40, 60, 84 for n = 2..7) (`norm_two_kissing`,
  `rootShell_card_formula`). Dimension 3 gives the 12-sphere arrangement (`fcc_kissing`). These
  are constructions; optimality is not claimed.
* Volumes rescale as `V_n(λr) = λⁿ V_n(r)` (`ballVol_smul`). The dimension ladder
  `V_{n+2} = (2πr²/(n+2))·V_n` holds exactly (`ballVol_add_two`), and the table built from it
  equals the closed forms (`volTable_eq`). The Gaussian integral over ℝⁿ is `(√π)ⁿ`
  (`gaussian_integral_dim`).

### 6.4 Depth of the "count the open spokes" recursion
* Iterating φ from 360 or from 361 reaches 1 in exactly seven steps (`totient_tower_360`).
* **The depth law** (`tdepth_eq`). There is a weight `A` with `A(mn) = A(m) + A(n)`, `A(2) = 1`
  and `A(p) = A(p − 1)` for odd primes. For `n ≥ 2` the depth is `A(n)` if `n` is even and
  `A(n) + 1` if `n` is odd. This is a known theorem (H. Shapiro, 1943), now machine-checked here.
* Consequences: depth nearly adds under multiplication (`tdepth_mul`). An odd prime is one step
  deeper than its predecessor (`tdepth_prime`). Depth is squeezed between logarithms to bases 2
  and 3, `2^(d−1) ≤ n ≤ 2·3^(d−1)` (`tdepth_bounds`), with equality at `2·3^k`
  (`tdepth_two_mul_three_pow`).
* Worked values: `A(360) = A(8) + A(9) + A(5) = 3 + 2 + 2 = 7`, and `A(361) = 2·A(19) = 6`, plus 1
  for oddness (`weights_360_361`). There are exactly 215 depth-7 numbers, from 83 to 1458
  (`depth_seven_class` (nd)).

**What this teaches.** Every "go deeper" operation in the system is **exact and compatible**.
Refining never destroys earlier information: base-60 digits, flower addresses, and dial bearings
(§7) all nest. Scaling a structure is a multiplication in some norm, so depth behaves like a
logarithm. That is literally true for the φ recursion, where the depth is bounded by `log₂` and
`log₃`.

---

## 7. Pillar VI: where the continuum enters

**What is proved**
* **All dials sit compatibly on one circle.** Refining a dial `N → M·N` (for example one more
  base-60 place, `M = 60`) sends each bearing to the same point of the unit circle, and no two
  bearings merge (`dial_refine_toCircle`, `dial_refine_injective`).
* **Three kinds of rotation space, distinguished by which turn orders they allow.**
  * lattices: only orders 1, 2, 3, 4, 6 (`lattice_rotation_trace`), so no lattice has a 5-fold
    turn (`no_lattice_pentagon`);
  * a finite dial: exactly the divisors of its size (`cyclic_rotation_iff`); the 360 dial has both
    5- and 6-fold turns (`dial_hosts_both`);
  * the continuous circle: every order.
* **The irrationalities that appear at the interface.** `√π` is irrational (`irrational_sqrt_pi`).
  `2cos 72° = (√5 − 1)/2` (`two_cos_two_pi_div_five`, `cos_pi_div_five_eq`). This is where the
  golden ratio enters, and because it is not an integer no lattice can carry the 5-fold turn. Twelve fifths never equal seven octaves (`three_pow_ne_two_pow`), and the
  comma is about 23.46 cents (`comma_cents`). The square root of a prime is irrational
  (`sqrt_prime_irrational`).
* **The precision budget is known in advance.** If radii are at most `60^m` and π is known to
  `k + m` base-60 places, then every side `s = r√π` is correct to `k` places (`side_precision`). If
  each table entry `√p` has relative error `ε`, then `√n` assembled from them has relative error at
  most `(1+ε)^k − 1`, where `k` is the number of distinct primes of `n` (`sqrt_eq_table`,
  `sqrt_table_error`).

**What this teaches**
* **π lives only at the interface.** Inside the dials, rods, lattices and base-60 arithmetic,
  everything is exact integer arithmetic. π appears once a bearing is placed on the continuous
  circle, or once volume is measured in ℝⁿ (one factor of π for every two dimensions). The
  irrationality results say that this interface cannot be made exact. The precision theorems say
  that its cost is known before the calculation starts.
* **Three different "non-closures".** Earlier write-ups merged these into one. The proofs show
  they are three mechanisms:
  1. *divisibility in a dial:* 7 ∤ 360, the wheel of fifths, the removed centre. Here the
     non-closing element is exactly the generator (a theorem, §2);
  2. *the continuum interface:* the irrational `√π`, the non-integer `2cos 72°`, and the comma
     (from unique factorisation: `3^a ≠ 2^b`);
  3. *topology / algebra:* the half-angle only returns after 4π (`halfAngle_add_four_pi`), there
     is no continuous square root on the circle (`no_continuous_sqrt_on_circle`), the 360 dial
     does not split as a 180 dial plus a polarity bit (`twist_not_split`), and zero has no
     log-polar coordinate.

  Only the first carries the "the odd one out generates" theorem. For the other two it is an
  analogy.

---

## 8. The boundaries: what the system provably cannot do

A distinctive part of this body of work is its **no-go theorems**. They mark exactly where the
exact, table-driven approach stops.

| Limit | Theorem |
|---|---|
| No single encoding turns both + and × into one vector addition injectively, and zero cannot be included | `no_single_encoding`, `no_mul_to_add_with_zero` |
| No continuous square root on the circle; halving on the dial has two answers 180 apart | `no_continuous_sqrt_on_circle`, `halving_two_valued` |
| The perspective divide is not affine, so no precomputed matrix removes it | `perspective_not_affine` |
| Uniform scaling leaves the projected image unchanged, so rendering at another scale saves nothing | `project_scale_invariant` |
| The unit ball fills a vanishing fraction of its bounding box as dimension grows | `ball_fraction_tendsto_zero` |
| Precomputation speedups tend to the ratio of per-vertex costs as scenes grow | `speedup_tendsto` |
| No lattice carries a 5-fold turn | `no_lattice_pentagon` |
| Base 60 divides exactly only by 2-, 3-, 5-smooth numbers | `isSexa_inv_iff` |

What *is* supported: drift-free rotation bookkeeping by integer dial indices (`rot_add`,
`rot_add_period`); log-polar multiplication one chart at a time (`logPolar_mul`,
`logPolar_injective`); precomputed prime-root tables with an error budget known in advance; and
exact base-60 fixed-point arithmetic for 5-smooth divisors.

---

## 9. Emergent patterns across the whole project

These are relationships that no single file states, but that the proofs establish when read
together.

1. **Splitting = a rotation fitting on a dial.** Lattice geometry (does a prime circle have
   points?) and dial arithmetic (does `k ∣ p − 1`?) are one fact (§3). This is the central link.
2. **One modulus, 12, decides both lattices**, because 12 = lcm(4, 6) (`two_lattice_fingerprint`).
3. **Generator = non-divisor** (`step_walks_iff_no_rotation`). This explains 7 on the 360 dial and
   7 on the circle of fifths in one statement.
4. **360 is the dial of the 19-board.** It is the multiplicative group of the 19-board, which is a
   field because 19 ≡ 7 (mod 12) (§4). The quarter turn is 90 of its steps.
5. **The same CRT split at several scales**: 360 → 8·9·5; 72 → 8·9; 144000 → 128·9·125; and the
   flower mod 7 → two rods.
6. **Centre removal at two scales**: `19² − 1 = 360` and `9² − 3² = 72`.
7. **2k points on a split circle**: 8 on the grid (k = 4), 12 on the flower (k = 6).
8. **Refinement is compatible everywhere**: base-60 digits, flower addresses and dial bearings all
   nest without loss (`sexaDigits_extend`, `addressL_append`, `dial_refine_injective`).
9. **π enters once per circle factor**: `(√π)ⁿ` for the Gaussian, and one π per two dimensions in
   the ball ladder.
10. **Self-reference changes the answer.** The board's 360 non-zero crossings form one dial. The
    360 dial's own 96 symmetries do not (their largest turn order is 12).
11. **Depth is a logarithm.** The φ-depth is additive up to parity and bounded by base-2 and
    base-3 logarithms.
12. **Observation (not a theorem):** the bases 2 and 3 of the depth bounds are the same pair as the
    octave and the fifth, whose mismatch is the comma. No theorem connects the two.

---

## 10. What is new or unique here, stated honestly

**What is not new.** The individual mathematical facts are, for the most part, known results:
Fermat's two-squares theorem, the splitting of primes in the Gaussian and Eisenstein integers, the
Chinese remainder theorem, cyclicity of finite-field units, the crystallographic restriction,
Schatunowsky's theorem, Shapiro's φ-iteration law, and the ball-volume formulas. Proving them is not
a claim of new mathematics.

**What is distinctive about this system:**

1. **A single architecture for a disparate set of motifs.** Sacred-geometry figures, a Go-style
   board, a 360° dial, base 60, an abacus, the circle of fifths, kissing spheres and hyperspheres
   look unrelated. The proofs show that they reduce to four ingredients (dial, two lattices, exact
   scaling, continuum interface), with rods connecting them, and that they interact in a fixed
   way. The reduction is backed by explicit theorems at each junction, not asserted.
2. **The recurring numbers 7, 12, 19, 360 are structurally determined, consistent with deliberate
   design.** Each one is the choice that makes the structure work (§1a):
   * 7: the smallest non-divisor of 360, hence the smallest generating step; also the prime at
     which the flower refines by `√7`.
   * 12: the lcm of the two lattices' turn orders, so the modulus of the fingerprint; also the
     largest turn order among the 360 dial's own symmetries.
   * 19: a class-7 prime (grid-inert, flower-splitting) whose square minus one is 360.
   * 360: the multiplicative dial of the 19-board.

   Each of these is a theorem. Where an earlier write-up of mine phrased something too narrowly
   ("unique to 19"), the precise class-level statement is given instead. It shows 19 as a member
   of a structured family, chosen from that family because `19² − 1 = 360`.
3. **π localised to one interface, with a known cost.** The system confines every
   irrationality to the step where a discrete structure meets the continuum, and proves how many
   digits that step needs. This matches your approach of treating π as a constant known to a
   chosen depth: the proofs justify it and give the depth required.
4. **A clear map of possible versus impossible.** The positive results (exact rods, compatible
   refinement, drift-free dial rotation, error budgets fixed in advance) sit next to proved limits
   (no universal + / × encoding, no continuous square root, no affine perspective, no lattice
   pentagon, the dimensional culling collapse). Few informal frameworks come with both sides
   proved.
5. **Machine-checked end to end.** About 520 declarations, all compiled without `sorry` and with
   only Lean's standard axioms. Every claim in this document can be re-checked by building the
   project. The few finite enumerations that use compiled evaluation are marked (nd).
6. **A corrected record.** Technical slips were found by the same process and are corrected
   rather than hidden (§0, `AUDIT.md`). As a result, every structural claim that remains is backed
   by a proof.

---

## 11. What the results mean for computation

* Use **integer dial indices** for orientation. Composition is index addition and cannot drift
  (`rot_add`). The benchmark in `bench/` (machine-specific, not formally verified) showed float
  matrices drifting while dial indices returned exactly to 0.
* Use **rods** for parallel, carry-free arithmetic modulo 360 or 144000.
* Use **prime-root tables** for square roots. The error bound is known before computing.
* Use **base 60** for exact fixed-point arithmetic whenever divisors are 5-smooth. Anything else
  needs a chosen depth, and `side_precision` tells you which depth.
* Do not expect savings from rescaling a scene, from removing the perspective divide, or from
  adding dimensions. These are proved limits.

---

## 12. Open directions

* The flower half of M4: "√p is a flower similarity ⇔ p is a flower norm" is proved only for
  `p = 7`. The general statement (every `p ≡ 1 (mod 3)` is `x² − xy + y²`) is the natural next
  theorem.
* ~~A group-theoretic statement of the rods principle for turn orders~~: proved later as
  `RodOrders.orderOf_eq_lcm_rods` (and `RodOrders.orderOf_360_eq_lcm_rods` for the rods 8, 9, 5 of
  the 360 dial).
* Known results not formalized here: the hairy ball theorem, Lindemann's theorem (π
  transcendental), torus-knot invariants, the icosahedral group being `A₅`, and Gauss–Wantzel.
  (The general four-circle Descartes theorem and five-sphere Soddy theorem were proved later:
  `DescartesGeneral.descartes_circle_theorem`, `DescartesGeneral.soddy_sphere_theorem`.)
* Empirical speed claims: only the single-machine benchmark exists. A GPU-scale comparison with a
  standard engine would be needed.

---

### File index (by pillar)

| Pillar | Files |
|---|---|
| I Dial | `CircleDivided`, `Temporal`, `SpokeCensus`, `KissingGears`, `RecursiveDepth` |
| II Lattices | `GaussianCircle`, `FlowerOfLife`, `SelfSimilar`, `RecursiveDepth`, `Synthesis` |
| III Board field | `Board`, `BoardField`, `FiniteField` |
| IV Rods | `ResidueAbacus`, `Abacus`, `KissingGears` |
| V Scaling | `Sexagesimal`, `FlowerOfLife`, `KissingLadder`, `KissingSpheres`, `SharedModel`, `HyperGamma`, `TotientDepth`, `DivisorCount`, `HighlyCompositeStructure` |
| VI Continuum | `Bridge`, `Explorer`, `NegativeSpace`, `Music`, `PitchCircle`, `Dodecahedron`, `PrimeRootTable`, `Bisection` |
| Boundaries | `VectorArithmetic`, `ClockFold`, `Projection` |
| Geometry side results | `Descartes`, `DescartesLine`, `Misc` |