# The shared model: how the formulas connect, stated as checked theorems

This document follows the first audit (`AUDIT.md`). The audit checked each claim on its own.
Here the aim is the one you asked for: show how the formulas depend on each other inside one
model, and check those connections in Lean. Each item names the Lean file and theorem. Everything
listed builds with no `sorry` and no added axioms. Two theorems (the Folio XI census and the
earlier count below two million) use compiled evaluation (`native_decide`).

A note on π, since the first audit misread you here. Nothing below tries to "prove π". π is
treated as what you describe: a constant known to some depth, which can be extended when more
precision is needed. The theorems say what that depth guarantees and how extending it works.

---

## 1. Terminology map

This is how I read your terms against standard mathematics. It is my interpretation, offered so
you can correct it where I have misunderstood the intended structure.

| Your term | Standard structure | Where it is checked |
|---|---|---|
| Circular space of the primes; spokes | Residues mod 360 (`ℤ/360`). Open spokes are the 96 units; shut spokes are the rest | `CircleDivided`, `SpokeCensus`, `FiniteField` |
| Primes living on circles in the square grid | Gaussian integers: a prime `p` sits on the circle `x² + y² = p` through grid points iff `p = 2` or `p ≡ 1 (mod 4)` | `GaussianCircle` |
| Quadrature | (a) squaring the circle, `s = r√π`; (b) the 90° relation between axes, i.e. multiplication by `i` | `Bridge`, `GaussianCircle.quarter_turn` |
| Dualistic relationship oscillating across axes | The quarter turn `(x, y) ↦ (−y, x)`. Two turns flip both axes (`i² = −1`), four return to the start (`i⁴ = 1`). With the axis swap this gives the 8 symmetries of the square | `GaussianCircle.quarter_turn_cycle`, `card_circlePoints_prime` |
| Negative space between circle and square | The set differences disc∖square and square∖disc | `NegativeSpace` |
| Self-similar structure, fractal partitions | Nested positional refinement: each level splits a cell into 60 (or `B`) sub-cells. Refining never changes the digits already fixed | `Sexagesimal.sexaDigits_extend`, `baseDigits_extend` |
| Scaled constants; precision fixed up front | Fixed-point integers `⌊c · 60^k⌋` | `Sexagesimal.sexaDigits` |
| Depth of π | `⌊π · 60^k⌋`, the first `k` sexagesimal places | `Sexagesimal.pi_sexaDigits_five`, `polygonPi_sexa_places` |
| Abacus | A circular abacus is arithmetic mod `n`; a positional abacus is base-`B` digits | `ResidueAbacus`, `Abacus` |
| A set of abaci working together | The Chinese remainder theorem: mod 360 = independent rods mod 8, 9, 5 | `ResidueAbacus.abacus360` |
| Kissing spheres | Kissing configurations: 6 circles around 1 at 60° steps (hexagonal); 12 spheres around 1 (face-centred cubic) | `KissingSpheres` |
| Gaussian relationship and scaling factors | `∫ e^{−x²} = √π` per dimension, so `π^{n/2}` in `n` dimensions. This one constant also scales every ball volume | `SharedModel` |
| Highly composite numbers | More divisors than any smaller number. Their structure is fixed by the primes: exponents can only decrease along 2, 3, 5, 7, … | `HighlyCompositeStructure` |
| Regular (sexagesimal-friendly) numbers | 5-smooth numbers. These are exactly the divisors of powers of 60 | `CircleDivided.dvd_pow_sixty_iff`, `Sexagesimal.isSexa_inv_iff` |
| Resonance of a prime with a modulus | `p² ≡ 1 (mod m)` | `Temporal` |
| Colour and sound as extra dimensions on the same circle | The map from frequency ratio to angle `360°·log₂(x)` mod 360°. Octaves become full turns; stacking intervals adds angles | `PitchCircle` |

---

## 2. Base-60 scaled arithmetic and π at a chosen depth (`Sexagesimal.lean`)

**What is exact.** Numbers of the form `a / 60^k` form a ring (`sexaSubring`): sums, differences
and products of scaled values stay scaled and involve **no rounding at all**. Division by `n`
stays exact for every input iff `n` has no prime factors other than 2, 3, 5 (`isSexa_inv_iff`,
`isSexa_div_of_regular`). In any base `B`, division by `n` terminates iff every prime factor of
`n` divides `B` (`dvd_pow_base_iff`). The prime content of the base decides which divisions are
exact. This is the precise form of "using primes for scaling".

**Extending depth.** `sexaDigits x k = ⌊x·60^k⌋`. For `k ≤ m`, the `k`-place value is the
`m`-place value integer-divided by `60^(m−k)` (`sexaDigits_extend`). One more place just appends
one base-60 digit (`sexaDigits_succ`). Extending the depth of π therefore never invalidates work
done at the shallower depth. As a check, `π = 3;8,29,44,0,47…` (`pi_sexaDigits_five`), and the
two-place value is read off from it by integer division (`pi_sexaDigits_two`).

**Where the digits come from, circularly.** Archimedes' inscribed `2^(n+1)`-gons trap π in an
interval of width `4^(−n)` (`polygonPi_bounds`). Since `4³ = 64 ≥ 60`, **three doublings buy one
sexagesimal place**: `|π − polygonPi(3k)| < 60^(−k)` (`polygonPi_sexa_places`).

**Precision budget up front.** The error in `√π` is at most the error in π, because `√π > 1`
(`abs_sqrt_sub_sqrt_pi_le'`). So if all radii are at most `60^m` and π is known to `k + m`
places, every side `s = r√π` is correct to `k` places (`side_precision`). The required depth is
known before any calculation starts.

**One precise caveat.** Addition, subtraction and multiplication are exact in the scaled system.
Division by a non-regular number, square roots and π itself are exact only up to the chosen depth.
The theorems above give the bound for that depth, and the bound is what makes the depth
redefinable on demand.

## 3. One shared model for every dimension (`SharedModel.lean`)

* `∫_{ℝⁿ} e^{−‖x‖²} dx = (√π)^n` (`gaussian_integral_dim`): the Gaussian in `n` dimensions is the
  one-dimensional Gaussian raised to the `n`-th power.
* `V_{n+2}(r) = (2π r² / (n+2)) · V_n(r)`, with `V_0 = 1` and `V_1 = 2r` (`ballVol_add_two`,
  `ballVol_zero`, `ballVol_one`).
* `volTable` computes the whole table `V_0 … V_N` from this recurrence. Each new entry costs one
  multiplication by the shared factor `2πr²` and one division. `volTable_eq` proves that the table
  equals the closed-form volumes **exactly**. This is the "shared model instead of isolation"
  point, stated precisely: the table needs one pass of `N` steps. Evaluating each `V_n` separately
  would need its own power of π and its own Gamma value every time. (The operation count is read
  off the definition; Lean checks the exactness, not the running time.)
* `V_n(1) · Γ(n/2+1)` equals the Gaussian integral over `ℝⁿ` (`ballVol_mul_gamma_eq_gaussian`),
  which links the ball and Gaussian formulas directly.
* Even dimensions need only integer powers of π: `V_{2k}(r) = π^k r^{2k} / k!` (`ballVol_even`).

## 4. Primes on circles in the square grid (`GaussianCircle.lean`)

* A prime is a sum of two squares iff it is 2 or `≡ 1 (mod 4)` (`prime_sum_two_sq_iff`).
* **Uniqueness:** the representation is unique up to order (`prime_sum_two_sq_unique`).
* Hence the circle `x² + y² = p` through a prime `p ≡ 1 (mod 4)` meets the grid in **exactly 8**
  points `(±a, ±b), (±b, ±a)` (`circlePoints_eq_octet`, `card_circlePoints_prime`). These 8
  points are one point together with its images under the 8 symmetries of the square. For a prime
  `≡ 3 (mod 4)`, such as 19, the circle meets **no** grid point (`circlePoints_eq_empty`).
* Multiplying Gaussian integers composes circles (`compose_circles`). The quarter turn is
  multiplication by `i` (`quarter_turn`, `quarter_turn_cycle`).

## 5. Negative space (`NegativeSpace.lean`)

Take a square of side `s` and the disc of radius `s/√π` on the same centre. They have equal area
(`volume_disc_eq_square`). The area of the disc outside the square is **exactly equal** to the
area of the square outside the disc (`negative_space_balance`). The general law behind it:
equal finite measure implies equal differences (`measure_diff_eq_of_measure_eq`).

## 6. Highly composite numbers are built from the primes in order (`HighlyCompositeStructure.lean`)

* In a highly composite number, a larger prime never has a larger exponent than a smaller prime
  (`factorization_antitone`, Ramanujan's condition). The proof is an exchange: swapping the two
  exponents would give a smaller number with the same number of divisors.
* The primes that occur form an unbroken run 2, 3, 5, … (`prime_dvd_of_lt`). Every highly
  composite number above 1 is even (`even_of_hc`).
* The link to the scaled system: highly composite numbers maximise the number of exact equal
  partitions available at a given size. Regular numbers are the ones whose reciprocals terminate
  in base 60. 60 and 360 are both. 144000 is regular but not highly composite (see `AUDIT.md`).

## 7. Arranged abaci: the Chinese remainder theorem (`ResidueAbacus.lean`)

* `ZMod 360 ≃+* ZMod 8 × ZMod 9 × ZMod 5` (`abacus360`), and likewise `ZMod 144000 ≃+* ZMod 128 ×
  ZMod 9 × ZMod 125` (`abacus144000`). Addition and multiplication run rod by rod with no carries
  between rods, and the rods recombine uniquely. This is the precise sense in which several small
  abaci can share one large calculation in parallel.
* Two numbers agree mod 360 iff they agree on every rod (`modEq_360_iff`, `modEq_144000_iff`).
* 19 sits at `(3, 1, 4)` and `19²` at `(1, 1, 1)`: it squares to 1 on every rod at once
  (`nineteen_on_rods`). Open spokes multiply across rods: `φ(360) = 4·6·4` (`totient_rods`).

## 8. Kissing arrangements (`KissingSpheres.lean`)

* Six unit circles around one: centres `2e^{iπk/3}` are at distance 2 from the centre and from
  each other (`hexCentre_norm`, `hexCentre_dist`), and six 60° steps close the circle
  (`hexCentre_six`). In Eisenstein coordinates the six neighbours are exactly the solutions of
  `a² − ab + b² = 1` (`eisenstein_units`).
* Twelve spheres around one (face-centred cubic): the 12 permutations of `(±1, ±1, 0)` touch the
  centre and do not overlap each other (`fcc_kissing`). Each touches exactly 4 others in the shell
  (`fcc_shell_contacts`).

## 9. Sound and colour on the same circle (`PitchCircle.lean`)

A ratio `x` goes to the angle `360°·log₂ x` on the 360° circle. Octaves land on the same point
(`pitchClass_two_mul`). Stacking intervals adds angles (`pitchClass_mul`). Each equal-tempered
semitone is exactly 30°, one hour of the 12-hour wheel (`semitone_angle`, `et_step_angle`). The
pure fifth sits at 210.585°–210.588° (`fifth_angle_bounds`). Angle is cents scaled by 3/10
(`pitchAngle_eq_cents`), so the Pythagorean-comma results in `Music.lean` carry over directly.

## 10. Items the first audit left open, now done

| Item | Result |
|---|---|
| Folio XI: primes spread evenly over the 96 open spokes up to five million | **Verified** (`SpokeCensus`). 348 513 primes below 5 000 000. Every open spoke holds between 3 572 and 3 685 of them, and both extremes occur. The spread is `113/3572 ≈ 3.2 %`, matching "barely three parts in a hundred". Only 2, 3 and 5 fall on shut spokes. The one-pass tally is proved to count exactly the primes on each spoke (`spokeTally_get`); the numbers come from compiled evaluation |
| Thesis curvature formula `k₄ = k₁ + k₂ ± 2√(k₁k₂)`: previously algebra only | **Proved geometrically** (`DescartesLine`). Take three circles resting on a line and touching in pairs. If the third sits between the other two, `1/√r₃ = 1/√r₁ + 1/√r₂`, giving the `+` sign. If it sits outside, the sign is `−`. Either way the Descartes relation holds with the line as curvature 0 (`descartes_with_line`) |

## Still not formalized

The hairy ball theorem, the transcendence of π (Lindemann), torus-knot invariants and the general
four-circle and five-sphere Descartes theorems are established results. None of them is available
in Lean's library, and each would be a substantial separate project. The benchmark and scoreboard
numbers are still unverified, because no data was supplied.