# Forensic audit, part 3: prime scaling, vector arithmetic, the folded clock, and rendering

This part tests five claims:

1. Prime scaling shapes how π and square roots scale.
2. All of arithmetic can be done as vector addition with polarity, using quadrature.
3. The clock is an ouroboros: a Möbius loop folded onto a `2π` dial, whose quadrants fold like origami.
4. Precomputed circular/prime scaling speeds up rendering and camera projection in real-time first-person games.
5. A hyper-dimensional model tracks objects and projects camera space more efficiently than standard designs.

Each point is marked in one of three ways:

- **Proved**: a Lean theorem, compiled with no `sorry` and no added axioms. The theorem name is given.
- **Measured**: an empirical micro-benchmark. It depends on this machine and compiler, and is **not** formally verified.
- **Not established**.

New Lean files: `RequestProject/PrimeRootTable.lean`, `VectorArithmetic.lean`, `ClockFold.lean` and `Projection.lean`. The benchmark is in `bench/projection_bench.c`, with raw output in `bench/results.txt`.

---

## Summary

| Claim | Verdict |
|---|---|
| Primes decide how square roots scale | **Proved.** Each `√n` is an integer times a product of `√p` over distinct primes. A prime-root table therefore gives every root, with an error budget known in advance. |
| Primes decide how rotation tables scale | **Proved.** The basic entry of an `N`-step table has algebraic degree `φ(N)`, which is 96 for 360 steps. |
| Subtraction is addition of a polarity-flipped vector | **Proved.** A polarity flip is a half-turn: `−z = e^{iπ}z`. |
| Multiplication and division are vector addition | **Proved for non-zero numbers,** in log-polar coordinates (magnitude axis plus polarity bit or clock angle). |
| *One* vector addition can carry +, −, × and ÷ together | **False.** Proved impossible: two charts are always needed, and zero has no log-polar coordinate. |
| The clock is a Möbius-type double cover | **Proved in the precise sense below.** Half-angles need `4π` to close, and there is no continuous square root on the dial. The 360-dial is not a 180-dial plus an independent polarity bit. |
| Quadrant folding with polarity bits loses nothing | **Proved.** |
| Circular (quadrature) rotation is cheaper per vertex than matrices | **False.** It is exactly the same arithmetic (proved). Measured cost is equal or slightly higher. |
| Precomputed scaling removes the perspective divide | **False.** The divide is not affine (proved). |
| Rendering a scene at a different scale saves work | **False.** The projected image is scale-invariant (proved), so scale is irrelevant to cost. |
| Precomputing per-frame constants speeds up big scenes | **Vanishing benefit.** The speedup tends to the per-vertex cost ratio (proved). Measured: a gain of up to 13% at 100 vertices, which shrinks with scene size except for cache effects. |
| Tables help when every object has its own orientation | **Measured, real:** about 2.3–3.3× faster in that kernel. |
| Dial-indexed camera turns never drift | **Proved exact.** Measured: 3.6 million float matrix products drifted to determinant 0.825. The dial index is exact. |
| Hyper-dimensional tracking is more efficient | **Not established.** Proved: the unit ball fills a fraction of its bounding box that tends to 0, so bounding-volume culling gets *worse* as dimension grows. |

---

## 1. How prime scaling affects square roots and π (`PrimeRootTable.lean`)

- **`sqrt_prime_irrational`, `prime_area_scale_irrational`.** Scaling an area by a prime `p` scales every length by `√p`, which is irrational. Scaling by `k²` scales lengths by exactly `k` (`square_area_scale`). The same holds with `s = r√π`: a prime scaling never keeps the side of the equal-area square rational relative to the old side.
- **`sqrt_eq_table`.** For every `n`: `n = m²q` with `q` squarefree, and `√n = m · ∏_{p | q} √p`. This is the exact sense in which "prime-based precomputation" works for square roots. A table of `√2, √3, √5, √7, …` gives any `√n` with at most `ω(n)` multiplications (`ω` = number of distinct primes), and no root extraction.
- **`prod_rel_error`, `sqrt_table_error`.** If every table entry has relative error ≤ `ε`, the assembled `√n` has relative error ≤ `(1+ε)^{ω(q)} − 1`. The precision budget follows from the factorisation alone, before any computation. This complements `Sexagesimal.side_precision` from the previous pass, which does the same for the depth of π.
- **`rootOfUnity_degree`, `totient_360`, `totient_256`.** The entry `e^{2πi/N}` of an `N`-step rotation table is algebraic of degree exactly `φ(N)`. This depends only on the primes of `N`: `φ(360) = 96`, `φ(256) = 128`.

  In the exact-arithmetic world, this is how prime structure scales π-based tables. A result I did **not** formalize: Gauss–Wantzel says the entries can be written with square roots alone exactly when `φ(N)` is a power of two. That holds for 256 but not for 360, so the 1° cosines cannot all be written with nested square roots.

  In floating point, all table sizes cost the same per lookup.

## 2. Arithmetic as vector addition (`VectorArithmetic.lean`)

- **Polarity is a half-turn.** `neg_eq_halfTurn`: `−z = e^{iπ}·z`. `quarter_quarter`: `i·i = −1`. `sub_eq_add_halfTurn`: `a − b = a + e^{iπ}b`. This is the precise content of "quadrature gives polarity".
- **Multiplication and division are vector addition, in log-polar coordinates.**
  - Reals: `logPolar x = (log|x|, polarity bit)`. Proved: `logPolar_mul`, `logPolar_div` and `logPolar_injective` for non-zero reals.
  - Complex numbers: `logAngle z = (log|z|, angle on the 2π clock)`. Proved: `logAngle_mul`, `logAngle_div` and `logAngle_injective`.

  Multiplying adds magnitudes on a log axis and adds angles on the dial. The polarity bit is the dial reduced to two positions.
- **The limit, proved.**
  - `no_mul_to_add_with_zero`: no injective encoding turns × into + once `0` is included.
  - `no_single_encoding`: no injective encoding of the reals turns **both** + and × into the same vector addition, even when × is only required away from zero.

  So "all arithmetic as one vector addition" needs two charts: the additive chart and the log-polar chart. Converting between them (`exp`/`log`) is exactly where the work of arithmetic goes, as on a slide rule. Your caution ("let's not get crazy converting all math like that") matches the mathematics. It does technically work chart by chart, but it cannot work in one chart, and the chart change is not free.

## 3. The clock as a folded loop (`ClockFold.lean`)

- **`halfAngle_sq`, `halfAngle_add_two_pi`, `halfAngle_add_four_pi`.** The half-angle point `e^{iθ/2}` squares to the dial point. One full `2π` turn of the dial sends it to its antipode (its polarity flips), and only two turns (`4π`) bring it back. This is the precise version of "the ouroboros is a Möbius loop folded to a 2π dial": the square-root level is a two-sheeted cover of the dial with a half-twist.
- **`no_continuous_sqrt_on_circle`.** No continuous function picks a square root of every point on the unit circle. Any square-root table on one dial needs a seam where polarity flips. This is a real constraint for anything that takes square roots of rotations, such as the circle–square bridge applied to angles, or half-angle interpolation.
- **`halving_two_valued`, `twist_not_split`.** On the 360-step dial, halving has two answers 180 apart. And `ZMod 360` is **not** isomorphic to `ZMod 180 × ZMod 2`: the polarity bit cannot be stored as an independent rod, because it must carry into the position.

  This is the discrete Möbius twist. It is the exact opposite of the coprime rods of `ResidueAbacus` (8, 9, 5), which never carry.
- **`fold_reflect_x`, `fold_reflect_y`, `unfold_fold`.** Folding the plane onto the first quadrant by `(x,y) ↦ (|x|,|y|)` identifies the four mirror images. The two polarity bits restore the original point exactly. The "origami" folding is lossless *with* the bits and lossy without them.

**Scope:** I proved the double-cover and non-splitting statements, which carry the mathematical content of the Möbius image. I did not formalize the Möbius band itself as a topological space.

## 4. Rendering and projection

### 4a. Proved (`Projection.lean`)

- **`project_scale_invariant`.** Perspective projection gives the same image for a scene scaled by any `λ ≠ 0`. This is why your normalized draw-space constants stay fixed across areas (THESIS2 §"common viewing frame"). The same fact means that choosing a "scaled graph" cannot reduce projection work.
- **`perspective_not_affine`.** `x/z` equals no formula `ax + by + cz + d` on `z > 0`. The per-vertex divide (or reciprocal) is unavoidable. Standard 4×4 homogeneous matrices already reduce it to one reciprocal per vertex.
- **`quadrature_eq_matrix`.** Rotating by multiplying with `e^{iθ}` performs exactly the four multiplications and two additions of the standard 2×2 rotation matrix. So the circular model *is* the standard model at the arithmetic level. It gives no per-vertex saving.
- **`rot_add`, `rot_add_period`, `norm_rot`.** With a rotation table in steps of `2π/N`:
  - composing turns is integer addition of indices;
  - indices wrap at `N`;
  - every entry has modulus exactly 1.

  Camera turns that are whole steps compose with **zero drift**.
- **`speedup_tendsto`.** With frame cost `s + n·c` (setup plus per-vertex cost), the speedup of one design over another tends to `c₁/c₂` as the vertex count `n` grows. Precomputing π, √π, √p or camera trigonometry changes only `s`. Its benefit therefore disappears in complex scenes unless it lowers `c`.

### 4b. Measured (`bench/projection_bench.c`, gcc 14 `-O2 -march=native`, one core; not formally verified)

Nanoseconds per vertex for camera rotation plus perspective projection:

| vertices | A: standard (libm trig per frame) | B: dial table per frame | C: quadrature (2 complex mults) | D: per-object trig | E: per-object table |
|---:|---:|---:|---:|---:|---:|
| 100 | 2.17 | 1.89 | 2.02 | 13.0 | 3.94 |
| 1,000 | 1.90 | 1.87 | 2.01 | 11.3 | 3.95 |
| 10,000 | 1.88 | 1.87 | 2.01 | 9.2 | 3.94 |
| 100,000 | 1.91 | 1.88 | 2.04 | 9.3 | 3.97 |
| 1,000,000 | 2.03 | 1.89 | 2.03 | 10.3 | 3.97 |

What the measurements say:

- **A vs B** (precomputed camera trig). About 13% faster at 100 vertices, and about 1% by 10,000. This is the amortisation theorem in action: the table saves four trig calls per frame, not per vertex. The 7% gap at one million vertices is most likely memory and cache noise. It is not a per-vertex saving, since the inner loops are identical.
- **C** (quadrature). Not faster than the matrix form, as `quadrature_eq_matrix` predicts.
- **D vs E** (per-object orientations: particles, crowds, foliage, projectiles). Here a dial table genuinely helps, at about 2.3–3.3× in this kernel. This is where precomputed circular scaling pays off in a game. Note that engines commonly already do this, with lookup tables, quaternions or GPU-side evaluation.
- **Drift test.** After 3,600,000 composed 0.1° turns (exactly 1000 revolutions), the float matrix product has determinant 0.825 and an entry error of 0.18. The integer dial index returns exactly to 0, with zero error.

  Caveat: production engines avoid this drift by rebuilding the camera matrix from stored angles each frame, or by renormalising quaternions. The dial gives exactness for free, but only for turns that are whole steps.

### 4c. What this means for real-time first-person games

Realistic benefits:

- **Exact, drift-free orientation bookkeeping.** Integer dial indices, composing by addition, are proved exact. They suit networked or deterministic lockstep games, where bit-identical replay matters.
- **Lookup tables for per-object orientations.** About 2.3–3.3× faster in the measured kernel.
- **Base-60 fixed-point coordinates.** From the earlier pass (`Sexagesimal`): +, −, × and division by 5-smooth numbers are exact, which gives exact, deterministic geometry for grid-aligned worlds.
- **Error budgets known in advance** (`sqrt_table_error`, `side_precision`). These let you pick the smallest safe precision.

Claims not supported:

- A per-vertex speedup of the projection itself: same arithmetic, and the divide is unavoidable.
- Savings from rendering at a different scale: the image is scale-invariant.
- Large frame-rate gains from precomputed constants in complex scenes: the gain tends to the per-vertex ratio, which is 1 here.

A full game-scale claim would need a prototype renderer profiled against a standard engine on the same scenes, including GPU execution. That is outside what can be verified here.

## 5. Hyper-dimensional tracking (`Projection.lean`)

- **`ball_fraction_step`, `ball_fraction_tendsto_zero`.** The unit ball fills a fraction `V_n(1)/2ⁿ` of its bounding cube. This fraction shrinks by at least the factor `π/4` every two dimensions and tends to 0.

  For a tracking model with many dimensions, this is the curse of dimensionality: bounding-sphere and grid culling reject less and less useful volume. Higher-dimensional state is still perfectly usable, since homogeneous 4D coordinates are the industry standard. But extra dimensions add cost rather than removing it, unless each one carries information that saves work elsewhere.
- The earlier `SharedModel.volTable_eq` still stands: the whole table of volumes across dimensions comes exactly from one shared recurrence.

## 6. What remains open

- A benchmark on real game scenes and GPUs. Only a single-core CPU micro-kernel was measured.
- Gauss–Wantzel (which table sizes allow square-root-only entries) is cited, not formalized.
- The Möbius band as a topological space, beyond the double-cover and non-splitting theorems proved here.
- The earlier open items (the hairy ball theorem, Lindemann's theorem, torus-knot invariants, general Descartes) are unchanged.