# Seven-level recursive reassessment of all the mathematics in this project

## 0. What changed, and how this document is organised

**Correction of a misreading.** In the previous pass (`SELF_SIMILAR_MODEL.md`) "depth 7" was
treated as a property of the mathematical object: seven base-ϖ digits of the flower, seven rings,
dimension 7, seven base-60 places. You meant it as the depth of *my own* recursion when examining
emergent properties and geometric relationships. The theorems in that section are still correct.
They are just not what you asked for, and the open item "define the depth-7 hyper-dimensional
object" is withdrawn: there was no such object to define.

**Method used here.** Each level examines the *relationships among the results of the level
before*, and asks what emerges that was not visible one level down:

| Level | Object examined | Question asked |
|---|---|---|
| 1 | every individual result (≈ 35 Lean files, 4 audit documents) | is it correct, and is it stated honestly? |
| 2 | pairs of results | which results say the same thing in two settings? |
| 3 | the pairwise links | which few mechanisms produce all the links? |
| 4 | the mechanisms | how are the mechanisms related to one another? |
| 5 | the relations between mechanisms | is there one invariant that decides them all? |
| 6 | the invariant against the continuous side (circle, π, dimensions) | where does the discrete structure stop and the continuum begin? |
| 7 | the whole analysis, applied to its own central object (the dial) | does the recursion close, and what is its fixed point? |

Conventions are unchanged. **Proved** means a Lean theorem that builds with no `sorry` and no added
axioms; the name is given. (nd) marks the older finite checks that use compiled evaluation
(`native_decide`); none of the new theorems use it. **Interpretation** is my reading and is not a
theorem. The new theorems are in `RequestProject/RecursiveDepth.lean`.

---

## Level 1 — every result on its own

Status of every earlier result was re-checked. The whole project builds; no `sorry`, no added
axioms. The **errors found in your source documents** are unchanged from `AUDIT.md` (inverse
derivative needs `x > 0`; explorer circles overlap; the Descartes formula quoted is the line case;
"`p − 1` divides every layer" is not special to 19; no temporal layer is highly composite; the
board's corners are crossings and the products are ±81; the `geom_sqrt` C code is circular;
"structured boundary effects" is not a stated result).

This pass found **four problems in my own earlier write-ups**. They are corrected here:

1. **"Depth 7" (SELF_SIMILAR_MODEL §3).** A misreading, as explained in §0. The theorems
   (`depth_seven_cells`, `seven_balls_cube`, …) stand as facts about the flower; they are not a
   "depth-7 object".
2. **"The prime that gives the flower its 19 circles is the same prime that makes the board a
   field" (SELF_SIMILAR_MODEL §3).** True, but it was presented as if unique to 19. It is not. At
   Level 5 below this becomes a theorem about a whole class of primes: 7, 19, 31, 43, 67, 79, …
   (`seven_nineteen_same_class`). Among the flower's own ball sizes the same happens for
   7, 19, 127, 271, 331 (`flower_board_primes`). What *is* unique to 19 is `19² − 1 = 360`
   (`Temporal.sq_sub_one_eq_360_iff`).
3. **"7 is the step that walks all 360."** True, but 96 different steps do that
   (`FiniteField.card_generating_steps`). What singles out 7 is that it is the *smallest* such
   step `> 1`, and also the smallest non-divisor of 360 (`seven_least_generator`). Level 4
   explains why those two are the same thing.
4. **"One non-closure pattern" (SELF_SIMILAR_MODEL §5).** That section put eight rows into one
   pattern. Examined more closely (Levels 3–6), the rows come from **three different mechanisms**:
   * divisibility in a dial (7 ∤ 360, the circle of fifths as a wheel, the excluded centre);
   * irrationality on the continuous side (`√π`, `2cos 72°`, and the comma, which comes from unique
     factorisation);
   * topology or algebra (the half-angle double cover, zero having no log-polar coordinate).

   For the first group, "the element that does not close is the one that generates" is now a
   theorem (`step_walks_iff_no_rotation`). For the other two groups it is only an analogy.

## Level 2 — pairs of results that say the same thing

| Link | Result A | Result B | What the pair shows |
|---|---|---|---|
| L2.1 | the 19-board mod 19 is a field (`BoardField.norm_ne_zero`) | the circle `x² + y² = 19` has no grid point (`GaussianCircle.circlePoints_eq_empty`) | same fact: `x² + y²` has no non-trivial zero mod 19 |
| L2.2 | the flower rescales by `√7` (`FlowerOfLife.hexNorm_scale`) | 7 splits into two mirror rods (`split_rods_bijective`) | a similarity of ratio `√7` exists *because* 7 splits |
| L2.3 | stepping by 7 walks the 360 dial (`walk_seven_eight`) | 7 ∤ 360 (`seven_wheel`) | generating and not dividing are one fact |
| L2.4 | circle of fifths: step 7 on 12 (`circle_of_fifths`) | 12 fifths ≠ 7 octaves (`Music.three_pow_ne_two_pow`) | the wheel closes, the frequencies do not; two mechanisms, not one |
| L2.5 | `GF(361)ˣ` cyclic of order 360 (`FiniteField.units_cyclic`) | the board's quarter turn is 90 dial steps (`BoardField.g_pow_ninety`) | the quarter turn `i` is the element of order 4 in a 360-dial |
| L2.6 | no lattice has a 5-fold turn (`Dodecahedron.no_lattice_pentagon`) | the 360-dial hosts 5- and 6-fold turns (`dial_hosts_both`) | lattice and dial allow different sets of turn orders |
| L2.7 | 12 points on a split-prime flower circle (`twelve_points` (nd)) | 8 points on a split-prime grid circle (`card_circlePoints_prime`) | `12 = 2·6` and `8 = 2·4`: twice the lattice's turn order |
| L2.8 | 360 → rods 8, 9, 5 (`ResidueAbacus.abacus360`) | TAB VII 72 → rods 8, 9 (`tab_seven_rods`) | the same CRT split at two scales |
| L2.9 | base-60 digits never change when depth grows (`sexaDigits_extend`) | the flower addresses: `j` then `k` digits = `j + k` digits (`addressL_append`) | refinement is compatible in both number systems |
| L2.10 | `V_{n+2} = (2πr²/(n+2))V_n` (`ballVol_add_two`) | `∫ e^{−‖x‖²} = (√π)^n` (`gaussian_integral_dim`) | π enters the dimension ladder once per circle factor |
| L2.11 | the flower ball sizes are hex norms (`shellCount_eq_hexNorm`) | 19 is a ball size (`flower_nineteen`) | explains why 19 sits on a 12-point flower circle |

## Level 3 — the few mechanisms behind all the links

Grouping the Level-2 links by what makes them true leaves five mechanisms:

* **M1 Dial orders.** In a cyclic group of size `N`, which orders occur and which steps generate.
  (L2.3, L2.5, L2.6-dial side)
* **M2 Splitting of primes in the two lattices** (square grid ℤ[i], flower ℤ[ω]).
  (L2.1, L2.2, L2.7, L2.11)
* **M3 Rods (CRT).** A dial of size `mn` with `gcd(m, n) = 1` is two independent dials.
  (L2.8)
* **M4 Exact similarity / refinement.** Multiplicative norms, compatible digit expansions, volume
  scaling. (L2.2, L2.9, L2.10)
* **M5 Continuous obstructions.** Irrationality of `√π` and `2cos 72°`, unique factorisation for
  the comma. (L2.4, L2.6-lattice side, L2.10)

## Level 4 — how the mechanisms are related (new theorems)

**M1 is one test.** A finite cyclic dial has a `k`-fold turn exactly when `k` divides its size:
`cyclic_rotation_iff`, with the special cases `zmod_rotation_iff` (the dial mod a prime, size
`p − 1`) and `field_rotation_iff` (any finite field, e.g. the 19-board `GF(361)`, size 360).

**M2 is M1 applied to the dial mod p.** This is the main emergent fact of the reassessment:

* `square_form_splits_iff`: for an odd prime `p`, `x² + y²` has a non-trivial zero mod `p` ⇔
  `p ≡ 1 (mod 4)` ⇔ `(ZMod p)ˣ` has an element of order 4 (a quarter turn).
* `hex_form_splits_iff`: for a prime `p ≠ 3`, the flower's form `x² − xy + y²` has a non-trivial
  zero mod `p` ⇔ `p ≡ 1 (mod 3)` ⇔ `(ZMod p)ˣ` has an element of order 3.

So a lattice with a `k`-fold symmetry (`k = 4` for the grid, `k = 3`, equivalently 6, for the
flower) *splits* at `p` exactly when its own rotation fits on the dial mod `p`. When it does not fit,
the rotation is instead added to the dial, and the board becomes a field with `p² − 1` positions,
where the rotation does fit. Every split-prime circle then carries `2k` points (L2.7).

**M3 is how M1 combines.** The orders available on a CRT product of dials are the lcm's of orders on
the rods (standard; not separately formalised here). 360 = 8·9·5 has no rod of size divisible by 7,
so no 7-fold turn: that is `7 ∤ 360` seen rod by rod.

**M4 depends on M2.** A similarity of a lattice of this kind with ratio `√p` is multiplication by
a lattice element of norm `p`, so it exists exactly when `p` is a norm. For the square grid this is
proved (`GaussianCircle.prime_sum_two_sq_iff`); for the flower only the direction used here is
proved (7 is a norm). That is why the flower refines by `√7`
(`hexNorm_varpi = 7`) and why the square grid has no similarity of ratio `√7` or `√19`
(`GaussianCircle.prime_sum_two_sq_iff`, `circlePoints_eq_empty`).

**M5 is not reducible to M1–M4.** It is the one mechanism that concerns the embedding of the dials
into the continuous circle. It is taken up at Level 6.

## Level 5 — one invariant (new theorems)

* **The class of `p` mod 12 decides both lattices at once** (`mod12_classification`). For a prime
  `p ≥ 5`: the board mod `p` is a field *and* the flower form splits at `p` ⇔ `p ≡ 7 (mod 12)`. The
  four classes 1, 5, 7, 11 mod 12 give the four combinations (split/inert in the grid × split/inert
  in the flower); the other three cases follow from the two Level-4 theorems by the same
  arithmetic, but only the class-7 case is stated as its own theorem. 12 appears because it is `lcm(4, 6)`, the lcm of the two lattices' turn orders.
* **7 and 19 are in the same class**, together with 31, 43, 67, 79 below 100
  (`seven_nineteen_same_class`). This is the precise content of "7 and 19 behave alike across the
  two lattices" (`SelfSimilar.seven_nineteen_two_lattices`).
* **Flower ball sizes.** `3k² + 3k + 1` is always a flower norm and `≡ 1 (mod 3)`, and it is
  `≡ 3 (mod 4)` exactly when `k ≡ 1, 2 (mod 4)` (`shellCount_mod_four`). So the prime ball sizes
  that make a board field are 7, 19, 127, 271, 331, … (`flower_board_primes`).
* **Generator ⇔ no turn of that order** (`step_walks_iff_no_rotation`). For a prime step `q` on a
  dial of size `N`: `q` walks the whole dial ⇔ `q ∤ N` ⇔ the dial has no `q`-fold turn. On the
  360-dial the smallest such prime is 7, and every step 2–6 divides 360, so 7 is also the smallest
  generating step (`seven_least_generator`).
* **Which turns fit on the board of side `p`** (`board_dial_rotation_iff`). For primes `p` and `q`,
  `q ∣ p² − 1` ⇔ `p ≡ ±1 (mod q)`. For 19 this gives turns of order 2, 3, 4, 5 but not 7, since
  `19 ≡ 5 (mod 7)`. The smallest field-board (`p ≡ 3 mod 4`) with a 7-fold turn is 43
  (`nineteen_board_turns`).

**Interpretation.** Everything discrete in your material (boards, flower, dials, rods, wheel of
fifths) is decided by *divisibility of the dial size* together with *the class of the prime mod 12*.
The special role of 360 = 19² − 1 comes from 19 being in the class 7 (mod 12), so the board is a
field, and from `19 ≡ −1 (mod 5)`, which adds the 5-fold turn.

## Level 6 — the discrete side meets the continuum (new theorems)

* **All dials sit compatibly on one circle** (`dial_refine_toCircle`, `dial_refine_injective`).
  Refining a dial `N → M·N` (for example one more base-60 place, `M = 60`) sends bearing `k` to
  `M·k`, which is the same point `exp(2πik/N)` of the unit circle, and no two bearings merge. So the
  base-60 depth structure (M4) and the dials (M1) are one nested family on the circle.
* **The three kinds of "rotation space" differ exactly in which orders they allow.**
  * lattice: orders 1, 2, 3, 4, 6 only (`Dodecahedron.lattice_rotation_trace`);
  * finite dial: the divisors of its size (`cyclic_rotation_iff`);
  * continuous circle: every order.

  The five-fold turn lives on the dial and on the circle but never on a lattice
  (`no_lattice_pentagon`). This is where the golden ratio enters (`cos_pi_div_five_eq`).
* **π lives only at this interface.** Inside the dials everything is exact integer arithmetic.
  π appears the moment a bearing is placed on the continuous circle, or a volume is taken in ℝⁿ
  (`ballVol_add_two`, `gaussian_integral_dim`, one factor π per two dimensions). How many digits
  of π are needed is fixed in advance by the refinement depth (`Sexagesimal.side_precision`). M5
  (irrationality of `√π`, `2cos 72°`) is the statement that this interface cannot be made exact.
* **Dimensions.** The same scaling that refines a dial moves between dimensions: `V_n(λr) = λⁿV_n(r)`
  (`KissingLadder.ballVol_smul`), and the kissing shell of squared-length-2 vectors works in every
  dimension (`norm_two_kissing`). No new mechanism appears; the ladder is M4 + M5.

## Level 7 — the recursion applied to itself (new theorems)

The central object of Levels 4–6 is the dial. Level 7 applies the same question ("which turns fit,
and what generates?") to the *dial's own symmetries*, the 96 open spokes of 360 under
multiplication:

* **The dial of the dial is not a dial.** Every open spoke satisfies `u¹² ≡ 1 (mod 360)`
  (`open_spokes_exponent`). So no spoke reaches all 96, and the open spokes are not cyclic
  (`open_spokes_not_cyclic`). The largest turn order available is 12. This contrasts with the
  board field `GF(361)`, whose 360 non-zero elements *do* form one dial (`FiniteField.units_cyclic`).
  At the second level of self-reference, the 19-board keeps the dial structure and the bare
  360-dial loses it.
* **The recursion terminates in seven steps.** Iterating "count the open spokes" (Euler φ) gives
  `360 → 96 → 32 → 16 → 8 → 4 → 2 → 1` and
  `361 → 342 → 108 → 36 → 12 → 4 → 2 → 1`, both exactly seven steps (`totient_tower_360`). The
  board's tower passes through 12. Seven steps does not single out 360 or 361, but *why* they share
  it has an exact answer, which is a genuine self-similar structure (see "Level 7, continued" below).
* **Level 7, continued: the depth of the recursion is a logarithm** (`RequestProject/TotientDepth.lean`).
  Write `tdepth n` for the number of φ-steps from `n` to 1.
  * *Shapiro's law* (`tdepth_eq`, worked values in `weights_360_361`). There is a completely additive weight `A`, meaning
    `A(m·n) = A(m) + A(n)`, with `A(2) = 1` and `A(p) = A(p − 1)` for odd primes. For `n ≥ 2`,
    `tdepth n = A(n)` when `n` is even and `A(n) + 1` when `n` is odd.
  * So depth adds under multiplication, up to a parity correction (`tdepth_mul`), and
    `tdepth p = tdepth (p − 1) + 1` for odd primes (`tdepth_prime`).
  * *Depth is squeezed between base-2 and base-3 logarithms* (`tdepth_bounds`):
    `2^(d−1) ≤ n ≤ 2·3^(d−1)` where `d = tdepth n`. The upper bound is attained exactly at
    `2·3^k` (`tdepth_two_mul_three_pow`). The bases are 2 and 3, the same pair as the octave and the
    fifth whose mismatch is the Pythagorean comma. That is an observation; no theorem links the two.
  * *The depth-7 class* (`depth_seven_band`, `depth_seven_class` (nd)). Every depth-7 number lies
    between 64 and `1458 = 2·3⁶`. There are exactly 215 of them, from 83 to 1458. Being in the band does
    not by itself force depth 7; other depths overlap it. For 360 and 361 the law gives the depth
    directly. `A(360) = A(8) + A(9) + A(5) = 3 + 2 + 2 = 7`, and 360 is even, so its depth is 7.
    `A(361) = 2·A(19) = 2·A(18) = 2·3 = 6`, and 361 is odd, so its depth is `6 + 1 = 7`.
* **Fixed point.** Going to an eighth level (asking the Level-4 question about the Level-7 groups)
  produces nothing new. The answer is again "divisors of the size, and the class of the prime".
  The recursion has closed. The stable content of all the mathematics in this project is:
  1. the divisor structure of the dial size (M1, M3);
  2. the class of the prime mod 12, i.e. how it splits in the square grid and in the flower (M2);
  3. exact multiplicative scaling (M4);
  4. π and the irrationalities, arising only where a dial is placed on the continuous circle or in
     ℝⁿ (M5).

## Reassessment table: every Lean file, by the level where it matters

| File | Level-1 status | Mechanism | Deepest level at which it contributes |
|---|---|---|---|
| `Bridge`, `Explorer`, `NegativeSpace` | proved (explorer circles overlap) | M5, M4 | 6 (π at the interface) |
| `HyperGamma`, `SharedModel`, `KissingLadder` | proved | M4, M5 | 6 (dimension ladder) |
| `Descartes`, `DescartesLine` | proved; line case only | M4 | 2 |
| `Bisection`, `Sexagesimal` | proved | M4 | 6 (refinement on the circle) |
| `Temporal`, `HighlyCompositeStructure` | proved; two source claims false | M1, M3 | 5 (`19² − 1 = 360`) |
| `DivisorCount`, `CircleDivided`, `SpokeCensus` | proved ((nd) for the census) | M1 | 7 (open spokes, φ-tower) |
| `Board`, `BoardField`, `FiniteField` | proved; corner claims false | M1, M2 | 7 (cyclic board vs non-cyclic spokes) |
| `GaussianCircle`, `FlowerOfLife`, `SelfSimilar` | proved; "unique to 19" corrected | M2, M4 | 5 (class mod 12) |
| `Abacus`, `ResidueAbacus`, `KissingGears` | proved | M3, M1 | 4 |
| `Music`, `PitchCircle` | proved | M1 (wheel), M5 (comma) | 5 (generator ⇔ non-divisor) |
| `Dodecahedron`, `KissingSpheres` | proved; `A₅` cited | M5, M1 | 6 (lattice vs dial vs circle) |
| `PrimeRootTable`, `VectorArithmetic`, `ClockFold`, `Projection` | proved | M4, M5, topology | 6 |
| `Misc` | proved (arithmetic) | – | 1 |
| `RecursiveDepth` (new) | proved | all | 4–7 |

## Still not established

* Hairy ball, Poincaré–Hopf, torus-knot invariants, Lindemann (π transcendental), the icosahedral
  group being `A₅`, Gauss–Wantzel: known results, not formalised here.
* The empirical scores and speed claims: no data beyond the machine-specific benchmark in
  `bench/`.
* The Level-7 "fixed point" statement is an assessment of the analysis. It is not a single
  theorem. What is proved is each of its components listed above.