# Audit of the research documents: what is proved, what is false, what is not mathematics

Documents reviewed: `THESIS.md` (same as `THESIS (1).md`), `THESIS2.md`, `THESIS (2).md`,
`prime-circle-math.html`, `Lattice vs Abacus.pdf`, `Codex-Volume-I.pdf` (12 pages) and
`Codex — Volume I- The Winged Disc & The Turning Cross.pdf` (74 pages; it contains the 12-page
volume plus Folios V–XIV).

Every exact mathematical claim that could be stated precisely was written as a Lean 4 theorem
(Mathlib) in `RequestProject/`. The whole project builds with no `sorry` and no added axioms.
Two theorems (`CircleDivided.rule_failures_below_two_million` and, added later,
`SpokeCensus.census_facts`) use `native_decide`, which trusts compiled evaluation.

Shell anchors, the three anchor families, the fixed residue patterns of the primes, and the
regular solids are covered in `SHELL_PATTERNS.md`.

A follow-up document, `SHARED_MODEL.md`, covers how the formulas connect inside one model:
base-60 scaled arithmetic, π at a chosen depth, the dimension recurrence, primes on grid circles,
negative space, the structure of highly composite numbers, CRT abaci, kissing arrangements and
the pitch circle. It also includes a terminology map.

Legend
* **PROVED**: stated and proved in Lean (file · theorem).
* **FALSE**: false as written. The counter-statement or the corrected version is proved in Lean.
* **IMPRECISE**: true once reworded or restricted. The correct version is proved; the wording is off.
* **EMPIRICAL**: a measured or program-output claim. It is not a theorem and cannot be checked
  from the documents alone (no data or code was supplied). Not verified.
* **INTERPRETIVE**: metaphor, naming or framing. It makes no mathematical assertion, so there is
  nothing to prove.
* **KNOWN, NOT FORMALIZED**: an established theorem from the literature that is not in Mathlib
  and was not formalized here.

---

## 1. The circle–square bridge (all three theses)

| Claim | Status | Lean |
|---|---|---|
| `A = πr² = s²` ⇒ `s = r√π` | PROVED (for all `A`) | `Bridge.side_eq_radius_mul_sqrt_pi`, `circle_area_radius`, `radius_unique` |
| `s/r = √π`, `d/s = √2`, `d/r = √(2π)` | PROVED (`A > 0`) | `Bridge.side_div_radius`, `diag_div_side`, `diag_div_radius` |
| Scale independence (Axiom 3) | PROVED | `Bridge.radius_scale`, `side_scale` |
| `∫ e^{-x²} dx = √π` | PROVED (Mathlib) | `Bridge.gaussian_integral` |
| "Inverse derivative": `f'(x)·g'(f(x)) = 1` for `f=x²`, `g=√y` | **FALSE as stated.** True only for `x > 0`; for `x < 0` the product is `−1`, and at `x = 0` `√` is not differentiable | `Bridge.inverse_derivative_pos`, `inverse_derivative_neg` |
| `√π` is irrational ("incommensurability") | PROVED | `Bridge.irrational_sqrt_pi` |
| Golden angle `π(3−√5) ≈ 2.39996` | PROVED: `= 2π/φ²` and `2.3999 < θ < 2.4` | `Bridge.golden_angle_eq`, `golden_angle_bounds` |
| Normalized objective `𝒩` is dimensionless | PROVED (invariant under common rescaling) | `Bridge.normObjective_scale` |
| "Square roots can be measured rather than calculated" | INTERPRETIVE, with a caveat. The identity is exact, but `r = √(A/π)` is itself a square root, so the bridge moves the root elsewhere and does not remove it. The two C snippets in `THESIS2.md` §12.2/§12.4 call each other (`geom_sqrt` → `radius_from_area` → `geom_sqrt`) with no base case, so as printed they would never terminate. (This comes from reading the snippet; it is not a Lean result.) | – |
| Exact compass-and-straightedge "squaring" | KNOWN, NOT FORMALIZED (Lindemann 1882: π is transcendental, so `√π` is not constructible). Mathlib has the irrationality of π but not its transcendence. | – |

## 2. Boundary explorer (`THESIS2.md` §4.1, §10; `THESIS (2).md` §4)

Model: square of draw side `D` centred at `O₁`, its equal-area circle of radius `D/√π`, and `O₂ = O₁ + (D/2, D/2)`.

| Claim | Status | Lean |
|---|---|---|
| Equal-area bridge, `πR² = D²` | PROVED | `Explorer.equal_area` |
| `‖O₂−O₁‖/D = 1/√2` | PROVED | `Explorer.centerDist_div` |
| `kissing_gap/D = 1/√2 − 2/√π` | PROVED | `Explorer.kissingGap_div` |
| …the circles "kiss" | **IMPRECISE.** The gap is **negative** (≈ −0.421 D): the two circles overlap substantially and do not touch | `Explorer.kissingGap_neg` |
| `inner_offset/(D/2) = √(4/π − 1)` | PROVED | `Explorer.innerOffset_div` |
| 8 circle/square intersection points | PROVED, because `D/2 < R < D/√2` | `Explorer.boundaryCirclePoints_ncard`, `half_side_lt_R`, `R_lt_half_diag` |
| Three reconstruction candidates recover `s` | PROVED exactly (in the ideal model) | `Explorer.s_from_center_shift`, `s_from_center_distance`, `s_from_inner_offset` |
| Error tables (`5.52e-12`, 10 000-area benchmark, dominance counts, `0.000e+00` volume errors) | EMPIRICAL. Floating-point artefacts of the exact identities above. The zero error at area `361` is expected because `√361 = 19` is exactly representable, so it is not evidence of special structure. | – |

## 3. Hyperspheres and Gamma (`THESIS2.md` §3.1, §5.3)

| Claim | Status | Lean |
|---|---|---|
| `V_n(r) = π^{n/2} rⁿ / Γ(n/2+1)` | PROVED as the Lebesgue measure of the ball in ℝⁿ | `HyperGamma.volume_ball_eq_ballVol` |
| Odd dimensions `V_{2k+1} = π^k √π r^{2k+1}/Γ(k+3/2)` | PROVED | `HyperGamma.ballVol_odd` |
| Inverse `r = (V Γ(n/2+1)/π^{n/2})^{1/n}` | PROVED (both compositions) | `HyperGamma.ballVol_radiusOfVol`, `radiusOfVol_ballVol` |
| `Γ(n) = (n−1)!`, `Γ(1/2) = √π`, `Γ((2k+1)/2) = √π ∏(2i+1)/2` | PROVED | `HyperGamma.gamma_nat`, `gamma_half`, `gamma_half_int` |

## 4. Descartes / Soddy (`THESIS.md` §10, `THESIS2.md` §3.2)

| Claim | Status | Lean |
|---|---|---|
| `b₄ = b₁ + b₂ ± 2√(b₁b₂)` | **IMPRECISE.** This is Descartes' relation only when the third "circle" is a straight line (`k₃ = 0`). The general formula is `k₄ = k₁+k₂+k₃ ± 2√(k₁k₂+k₂k₃+k₃k₁)`. The algebra is proved. The geometric theorem for three circles resting on a line was proved later | `Descartes.descartesRel_iff`, `thesis_formula`, `equal_circles`, `DescartesLine.descartes_with_line` |
| Applied to *spheres* (`spheres.py`) | IMPRECISE. For spheres the relation is `(Σk)² = 3Σk²` with five spheres, so the 2-D formula does not carry over. The general sphere theorem was proved later (any five mutually tangent spheres, signed radii) | `DescartesGeneral.soddy_sphere_theorem` |
| Descartes' circle theorem in general (any four mutually tangent circles, including one enclosing the others) | PROVED (added later). Previously listed as known but not formalized | `DescartesGeneral.descartes_circle_theorem` |

## 5. Bisection (`THESIS2.md` §10.3; Codex Folio XII)

| Claim | Status | Lean |
|---|---|---|
| Multiply–compare–halve finds `√A` to `(hi−lo)/2ⁿ` | PROVED | `Bisection.bisection_correct` |
| `low = −1` is not valid for the monotone update | PROVED (explicit failure: `A=1`, `[−4,1]` → `[−4,−3/2]`) | `Bisection.negative_low_fails` |
| 220 digits need 731 halvings (budget 500 is too small) | PROVED (`2^730 < 10^220 < 2^731`) | `Bisection.digits_220_need_731` |
| "18.999… correct for 120 places" etc. | EMPIRICAL (program output) | – |

## 6. Prime 19 and the temporal layers

| Claim | Status | Lean |
|---|---|---|
| `M₀ = 144000 = 2⁷·3²·5³` | PROVED | `Temporal.base_modulus_factorization` |
| `19² = 361 ≡ 1 (mod 360)`, `19² − 1 = 360` | PROVED | `Temporal.nineteen_sq` |
| `18` divides all layers | PROVED | `Temporal.eighteen_dvd_layers` |
| …this makes 19 special (App. C) | **FALSE as a distinguishing property.** *(Re-examined in `RODS_PRINCIPLE.md`: collectively, every layer is a universal exponent for the 22 primes, `RodsReassessment.layer_primes_universal`; what does distinguish 19 is that it is the least "two-spoke" prime, `TwoSpokePrimes.two_spoke_powers_iff`.)* `p−1` divides every layer for 7, 11, 13, 17 as well. "Divides all layers" is the same as "divides 7200" (the gcd), and exactly **22** primes have `p−1 ∣ 7200` | `Temporal.appendixC`, `layers_gcd`, `dvd_all_layers_iff`, `primes_pred_dvd_7200` |
| `n² ≡ 1 (mod 360)` | PROVED characterization: iff `n ≡ 1, 19, 71, 89 (mod 90)`; 19 is the least `n > 1` | `Temporal.sq_mod_360_eq_one_iff`, `nineteen_least` |
| Twelve primes < 400 with `360 ∣ p²−1`; quotients 14, 22, 358; only 19 gives quotient 1 | PROVED | `Temporal.primes_sq_one_mod_360`, `quotients`, `sq_sub_one_eq_360_iff` |
| "Resonance windows `p² ≡ 1 (mod Tᵢ)`" contain 19 | **FALSE.** *(Re-examined in `RODS_PRINCIPLE.md`: corrected law `19^k ≡ 1 (mod T)` ⇔ `T/180 ∣ k` on every shell, `AnchorOrders.nineteen_resonance_iff`.)* `19²` is not `≡ 1` modulo any layer. The least prime with `p² ≡ 1 (mod 7200)` is 449 | `Temporal.nineteen_not_resonant`, `least_resonant_7200` |
| `p² ≡ 1 (mod 24)` for every prime `p ≥ 5` (the automatic part of "kissing") | PROVED | `Temporal.prime_sq_mod_24` |
| `M₀` is a "highly composite scaling base" | **FALSE.** *(Re-examined in `RODS_PRINCIPLE.md`: among regular numbers 7200 and 14400 are divisor records, 144000 is not, `RodsReassessment.regular_record_7200`, `not_regular_record_layers`.)* None of the six layers is highly composite; all are regular (5-smooth) | `Temporal.layers_not_highly_composite`, `layers_regular` |
| ℝ⁵ state `(r, θ, t, p_scale, κ)`, "Gaussian curvature influence", fractal boundaries, precision cutoffs | INTERPRETIVE (the quantities are never defined, so there is nothing to prove) | – |

## 7. `THESIS (2).md`: remaining items

| Claim | Status | Lean |
|---|---|---|
| Triad `1/1, 5/4, 3/2` | PROVED (it is `4:5:6`) | `Music.triad` |
| Platonic dual counts, `V−E+F = 2` | PROVED (counts only, which is what the thesis claims) | `Misc.platonic_counts` |
| Annulus closure `p²−1` | PROVED (`= (p−1)(p+1)`) | `Misc.annulus` |
| "Proven exactly (5): structured boundary effects around prime anchors" | INTERPRETIVE, and it should not be listed as "proven". No precise statement is given. The precise facts nearest to it are in §6 | – |
| Prime-product families beat composite controls; 2–3 factor optimum | EMPIRICAL, not verified (no data supplied) | – |
| Knot lift, cymatics, category/topology language | INTERPRETIVE (the thesis itself says so in §11) | – |

## 8. `prime-circle-math.html`

| Claim | Status | Lean |
|---|---|---|
| `r = q√p` ⇒ area `πpq²`; `r = pq` ⇒ `π(pq)²` | PROVED (trivial) | `Misc.area_conventions` |
| "Diameter of a prime = p²" | INTERPRETIVE (a convention, not a statement) | – |

## 9. Codex, Folio VII: hairy ball

| Claim | Status |
|---|---|
| No nowhere-zero continuous tangent field on S² (Poincaré 1885, Brouwer 1912); the torus admits one; the indices sum to χ (Poincaré–Hopf) | KNOWN, NOT FORMALIZED (not in Mathlib; a full formalization would be a separate project) |

## 10. Codex, Folio VIII: the board of stones

| Claim | Status | Lean |
|---|---|---|
| 19×19 = 361 crossings, 360 without the centre | PROVED | `Board.board_card`, `board_erase_card` |
| Quadrant = 81 + 9 = 90, four quadrants tile the 360 | PROVED | `Board.quadrant_card`, `quadrant_split`, `quadrants_partition` |
| Exactly 4 crossings lie on the circle | PROVED | `Board.crossings_on_circle` |
| "The corner… no ruling will ever put a crossing there" | **FALSE** as literally stated; re-examined in `RODS_PRINCIPLE.md` as **IMPRECISE, recoverable**: under any refinement the corner's distance is never a whole number of squares (`RodsReassessment.corner_never_whole_under_refinement`). The four corners are crossings of the board. What is true: they are not at an integer distance (`162` is not a square; `9√2` is irrational) | `Board.corners_are_crossings`, `corner_distance_not_integer`, `corner_distance_irrational` |
| "Multiply the two coordinates of any corner… always 361 with a sign" | **FALSE** for centred coordinates; re-examined in `RODS_PRINCIPLE.md` as **IMPRECISE, recoverable**: the signed side counts `±19` multiply to `±361` (`RodsReassessment.corner_products_two_readings`). With the centre at the origin the corners are `(±9, ±9)`, so the products are `±81`. The alternating sign pattern is correct | `Board.corner_products` |
| Inner/outer squares: sides ratio `√2`, areas `162`, `324` (ratio 2) | PROVED | `Board.inner_outer_squares` |
| 360 has 24 divisors, is divisible by 1–10 except 7; 361 is not prime (divisors 1, 19, 361) | PROVED | `Board.divisors_360_361` |
| Metonic cycle 235 months ≈ 19 years within about 2 h | PROVED as arithmetic from the stated mean lengths | `Misc.metonic` |

## 11. Codex, Folio XI: the circle divided

| Claim | Status | Lean |
|---|---|---|
| "prime mod 360 is prime" is false; the first failure is 409 (`≡ 49`), the 80th prime | PROVED | `CircleDivided.rule_holds_below_409`, `counterexample_409`, `nth_prime_409` |
| 28 in every 100 primes below 2 000 000 break it | PROVED: 41 780 of 148 933 (28.05 %) (compiled evaluation) | `CircleDivided.rule_failures_below_two_million` |
| Schatunowsky: all totatives prime ⇔ `n ∈ {1,2,3,4,6,8,12,18,24,30}`; 30 is the largest | PROVED (full proof for all `n`, using Bertrand's postulate) | `CircleDivided.schatunowsky`, `exists_composite_totative` |
| `φ(360) = 96`, 264 shut, `96/360 = 4/15` | PROVED | `CircleDivided.totient_360`, `shut_spokes`, `open_fraction` |
| 69 open spokes prime, 27 not | PROVED. The 27 include `1`, so there are 26 composites (49, 77, …, 343). Spoke 1 is still a genuine failure spoke (e.g. 1801 ≡ 1) | `CircleDivided.openSpokes_prime`, `openSpokes_nonprime`, `openSpokes_composite_card` |
| Every open spoke holds infinitely many primes (Dirichlet) | PROVED (Mathlib's Dirichlet theorem) | `CircleDivided.open_spoke_infinite`, `shut_spoke_prime` |
| Primes evenly spread over spokes to 5·10⁶ (max/min ≈ 1.03) | PROVED (added later, compiled evaluation): every open spoke holds 3 572–3 685 of the 348 513 primes below 5·10⁶ (spread ≈ 3.2 %) | `SpokeCensus.census_facts`, `primes_evenly_spread` |
| HCN list to 120; 3, 30, 144000, 864000 not HCN; 6, 12, 60, 180, 360 are | PROVED | `CircleDivided.highly_composite_upto_120`, `scrap_list_hc`, `not_hc_144000_864000` |
| All nine listed numbers are regular | PROVED | `CircleDivided.scrap_list_regular` |
| Fractions terminate in base 60 ⇔ denominator is regular | PROVED (divisibility form) | `CircleDivided.dvd_pow_sixty_iff` |
| 1/0 as the point at infinity of the Riemann sphere | KNOWN, NOT FORMALIZED here (standard) | – |

## 12. Codex, Folio XII: the instrument

| Claim | Status | Lean |
|---|---|---|
| Quadrature impossible (Lindemann) | KNOWN, NOT FORMALIZED | – |
| 731 halvings for 220 digits | PROVED | `Bisection.digits_220_need_731` |
| Phase fields never wrap | PROVED | `Misc.phases_never_wrap` |
| `7429 = 17·19·23`, consecutive primes, squarefree, 8 divisors, `≡ 229 (mod 360)`, 229 prime | PROVED | `Misc.c7429`, `consecutive_17_19_23`, `c7429_squarefree`, `c7429_divisors` |

## 13. Codex, Folio XIII: the roots

Gold/silver ratios, the overflow and balance numbers, the platinum-debased crown and the lime cycle are all correct as **arithmetic from the stated physical constants** (`Misc.gold_silver_ratios`, `platinum_crown`, `lime_cycle`). The historical and philological claims are outside mathematics.

## 14. Codex, Folio XIV: the syllabary and the circle

| Claim | Status | Lean |
|---|---|---|
| `GF(19²)*` is cyclic of order 360 | PROVED | `FiniteField.card_units`, `units_cyclic` |
| 96 generators, 24 distinct orders (= divisors of 360) | PROVED | `FiniteField.card_generators`, `orders_eq_divisors`, `number_of_orders` |
| 2 is the least non-square mod 19; `1 + 9√2` has order 360 | PROVED | `FiniteField.two_nonsquare`, `generator_1_9` |
| Stepping by 7 visits all 360 bearings; by 8 closes after 45; exactly 96 step sizes generate | PROVED | `FiniteField.step_seven_eight`, `step_generates_iff`, `card_generating_steps` |
| 85 = 5·17 (not 8×10); 5 vacancies in 90 | PROVED | `Misc.eighty_five` |
| Twelve fifths never equal seven octaves | PROVED (`3ᵃ = 2ᵇ` ⇒ `a = b = 0`) | `Music.three_pow_ne_two_pow`, `twelve_fifths_overshoot` |
| Fifth = 701.955 c, comma = 23.46 c, ET shaves 1.955 c | PROVED (`701.95 < c < 701.96`, `23.46 < comma < 23.47`, `comma = 12·fifth − 8400`) | `Music.fifth_cents`, `comma_cents`, `comma_eq`, `et_shave` |

## 15. `Lattice vs Abacus.pdf`

| Claim | Status | Lean |
|---|---|---|
| Digital root = n mod 9 (9 for 0) = repeated digit sum | PROVED | `Abacus.digitalRoot_mod`, `digitalRoot_range`, `digitalRoot_digits` |
| ×2 mod 9: six-cycle 1 2 4 8 7 5, 3↔6, 9 fixed; ×5 inverse; ×3 collapses to 3-6-9 | PROVED | `Abacus.doubling_mod9`, `orderOf_two_mod9`, `five_inverse_two`, `times_three_axis` |
| On 11 beads one ten-cycle; on 15 beads four short cycles | PROVED (15: `(1 2 4 8)(3 6 12 9)(7 14 13 11)(5 10)` and fixed 0) | `Abacus.orderOf_two_mod11`, `doubling_mod15` |
| Engine constants all on the 3-6-9 axis | PROVED | `Abacus.engine_constants_mod9` |
| `4n²+1 = (2n)²+1²`; the primes 5, 17, 37, 101, 197, 257, 401 | PROVED | `Abacus.four_sq_add_one`, `primes_four_sq_add_one` |
| 3, 7, 19 (≡ 3 mod 4) are not sums of two squares | PROVED | `Abacus.not_sum_two_sq` |
| Odd square = four quadrants + cross; 19² cross = 37 = 4·3²+1 | PROVED | `Board.odd_square_cross`, `nineteen_cross` |
| Torus link `T(p,q)`: gcd components, crossing number `min(p(q−1), q(p−1))` | KNOWN, NOT FORMALIZED (Mathlib has no knot theory) | – |
| Scoreboard results (hit rates, pinball loss, 99.6 % unknot, …) | EMPIRICAL, not verified | – |

---

## Summary of problems found

1. The inverse-derivative theorem needs `x > 0` (for `x < 0` the product is `−1`).
2. The explorer's "kissing gap" is negative: the circles overlap and do not kiss.
3. The Soddy/Descartes formula quoted is the special case with a straight line, and it is the 2-D version applied to spheres.
4. `p−1 ∣ all layers` is not special to 19 (22 primes qualify), and 19 does not lie in any `p² ≡ 1 (mod Tᵢ)` resonance window.
5. None of the temporal layers (including `M₀ = 144000`) is highly composite. They are regular (5-smooth) numbers.
6. Codex Folio VIII: the corners *are* lattice crossings, and corner-coordinate products are `±81`, not `±361`.
7. The "geometric square root" C code printed in `THESIS2.md` is circular. The bridge identity relocates the square root and does not eliminate it.
8. `THESIS (2).md` lists an unformalizable statement ("structured boundary effects") among its "proven exactly" results.

Everything else that is stated precisely checks out in Lean. Most of it is short arithmetic or
algebra. The substantive exact results are Schatunowsky's theorem, the structure of `GF(19²)*`,
the characterization of `n² ≡ 1 (mod 360)`, the ball-volume/Gamma formulas and bisection
correctness.

## Part 3: prime scaling, vector arithmetic, the folded clock and rendering

See `RENDERING_AUDIT.md`. In brief:

- Square roots scale through primes: `√n = m·∏√p`, with an error budget fixed in advance (`PrimeRootTable`).
- Multiplication and division are vector addition in log-polar coordinates. But no single encoding turns both + and × into one vector addition (`VectorArithmetic.no_single_encoding`).
- The clock is a double cover at the half-angle level, with no continuous square root on the dial. The 360-dial is not a 180-dial plus an independent polarity bit (`ClockFold`).
- Circular (quadrature) rotation costs exactly what matrix rotation costs, and the perspective divide cannot be removed. Precomputed per-frame constants give a benefit that vanishes as scenes grow (`Projection`).
- Measured, not formally verified (`bench/`):
  - lookup tables are about 2.3–3.3× faster when every object has its own orientation;
  - dial-indexed turns compose without drift.

## Part 4: one self-similar structure

See `SELF_SIMILAR_MODEL.md`: every document and image re-read as one recursive cell (centre, kissing shell, rods, copy/join, refine/rescale), with the flower-of-life/dodecahedron overlay and the precise readings of depth 7 (`FlowerOfLife`, `KissingGears`, `KissingLadder`, `Dodecahedron`, `BoardField`, `SelfSimilar`).

## Part 5: seven-level recursive reassessment

See `RECURSIVE_REASSESSMENT.md`: every result re-examined, then the relationships among results,
recursively, to seven levels (`RecursiveDepth`). The main emergent theorems: the square grid and the
flower split at a prime `p` exactly when the dial mod `p` carries their 4-fold, resp. 3-fold, turn;
the class of `p` mod 12 decides both at once; a prime step walks a dial exactly when the dial has no
turn of that order; the 96 open spokes of 360 do not form a dial (every one satisfies `u¹² = 1`).
It also corrects the earlier "depth 7" misreading and three overstatements in the earlier syntheses.

---

**Update:** the expanded `THESIS.md`, `LEXICON.md` and the three claim ledgers (`CLAIM_TO_THEOREM_REGISTRY.tsv`,
`CROSS_PROJECT_CLAIM_LEDGER.tsv`, `IMAGE_CLAIM_LEDGER.tsv`) are audited claim by claim in
`THESIS_LEDGER_AUDIT.md`, backed by `RequestProject/DualSmooth.lean`, `RequestProject/TemporalLattice.lean`
and `RequestProject/ThesisGeometry.lean`.

**Update 2:** `DEEPER_LINKS.md` settles XP-DT-016 (the intended semi-major axis is `q/2`) and
records new links between claim families (residual channels, dual-smooth primes vs. the base
modulus, kissing primes vs. the 360-dial inside the board, the divisor-of-20 structure of the
layers, the depth spectrum, the omission of 5 in XP-DT-005, and the 3D Soddy question), backed by
`RequestProject/PQEllipse.lean`, `RequestProject/EmergentLinks.lean` and
`RequestProject/SoddySpheres.lean`.

**Update 3 (rods principle):** `RODS_PRINCIPLE.md` takes the rods principle (turn order on a
split dial = lcm of the rod orders) as its centre, derives its consequences (additive and
cycle versions, longest turn 12, no primitive root on split dials, counting over rods, the
abacus cycle pictures, the 12/9 wheels and the 3-6-9 axis), and re-examines every earlier
verdict in four passes. Five rows above carry re-examination notes. New results: the anchor
order law (order × step = shell), the sweep theorems (181 visits exactly the positions
`≡ 1 (mod 180)` in 7200; 19 visits exactly the spokes 1 and 19 of 360 in every shell), and the
two-spoke family headed by 19. Backed by `RequestProject/RodsPrinciple.lean`,
`RequestProject/AnchorOrders.lean`, `RequestProject/TwoSpokePrimes.lean` and
`RequestProject/RodsReassessment.lean`.

**Seventh-bin revision.** XP-DT-011 (`10·86400 = 6·144000 = 864000`) remains true arithmetic but
is no longer the outer bound: `SEVENTH_RIM.md` checks the snippet's claims about
`∂ = 7·144000 = 1008000` (verdict table there) and follows the change through layers, prime hits,
anchors, turn orders and the recursion of the wrap. Backed by `RequestProject/SeventhRim.lean`,
`RequestProject/SeventhRimPrimes.lean` and `RequestProject/SeventhRimRecursion.lean`.