# Run 002 — independent recheck of the Operation Translation Series

**Agent:** 數學戰士「墜衡」, Claude Opus 5, AMRAL Research Lab
**Date:** 2026-08-14 (Asia/Taipei)
**Subject:** Neo.K, *Collatz Operation Translation Series* — SSSP Repaired v1.0
(nine core papers + Hard-Zeta research program), repair date 2026-08-14

## Role and boundary

Neo.K handed this arm the repaired series package and asked for the verification
role. This report is that: an **independent re-derivation** of the series' finite
claims. It is not co-authorship, it is not review of the research direction, and
it is not an assessment of whether the series' programme can close.

Re-deriving a finite claim confirms the finite claim. The series itself is
explicit that its finite results do not settle the conjecture, and nothing here
changes that. The subject's own `validation.json` carries the same warning, and
it is correct to.

The package was **not modified**. Its `AI_HANDOFF.md` forbids editing provenance
in place, and that rule was followed.

The subject package is now archived in this repository as its own top-level tree,
`../../collatz-ot-series-neok/`, byte-exact and
under Neo.K's authorship. It is a separate research tree from this one, and its
presence beside this report is not agreement between the two — the archived copy
still passes the package's own verifier, and
`../data/gate-logs/ot-package-integrity.txt` is that run against the committed
bytes.

## The two findings, up front

Everything mathematical in the six finite claim groups holds. Two defects are
worth the author's attention, neither of them mathematical:

1. **The package's own verifier cannot run to completion on the author's
   platform.** `tools/generate_math_inventory.py` writes UTF-8 JSON to stdout, so
   on a cp950 Windows host it aborts at step 7 of 9 on the `ö` of "Möbius". One
   line fixes it. §1.
2. **The published KL constant is 2.79 ULP from the real value** — it is the
   faithful output of the stated float expression, but not the nearest double, so
   its 17th significant digit is wrong. The subject's own assertion cannot detect
   this because it compares that float computation against itself. §7.

Both are reported, neither is fixed here: the package's `AI_HANDOFF.md` forbids
editing provenance in place, and patching it would change its hashes.

## 1. Package integrity — PASS, with a defect

Run as the handoff instructs:

```bash
python tools/verify_series.py .
```

it aborts at step 7 of 9:

```
FAIL: math inventory generation failed
UnicodeEncodeError: 'cp950' codec can't encode character '\xf6' in position 493071
```

`tools/generate_math_inventory.py` prints UTF-8 JSON to stdout. On a cp950
Windows host — the author's own platform — stdout cannot encode `\xf6`, which is
the **ö of "Möbius"** in Papers 07 and 08. Traditional Chinese survives cp950;
`ö` does not.

Under `PYTHONUTF8=1` the whole suite passes:

| Step | Result |
|---|---|
| required package files | PASS |
| checksums, complete payload | PASS (49 files) |
| strict UTF-8 + canonical `$`/`$$` policy, 10 sources | PASS |
| source-set aggregate vs SSSP anchor `96b1b9cc…` | PASS |
| per-file diffs + aggregate `repair.diff` regenerated byte-for-byte | PASS |
| finite/algebraic theorem regression reproduced | PASS |
| source-derived math inventory, 3027 formula hashes | PASS |
| MathJax | SKIP — dependency absent, and correctly labelled a skip rather than a fake PASS |
| manifest/validation scope consistency | PASS |

**This is a package defect, not merely an environment quirk.** A verifier its
own author cannot run to completion is not a working verifier. The minimal fix
is one line in `generate_math_inventory.py`:

```python
sys.stdout.reconfigure(encoding="utf-8")
```

The package's design is otherwise notably careful: the MathJax step refuses to
report a pass when its dependency is missing, and the diff regeneration is
mechanical rather than asserted in prose.

## 2. Paper 05 — the `k=16` block benchmark, reproduced independently

The subject claims: on `1 ≤ n < 2^20` with `k = 16`, **938,413** strict descents
and **exactly 2** equalities.

```json
{"k":16,"domain":"1 <= n < 1048576",
 "strict_descent":938413,"equality":2,"ascent":110160,
 "equality_witnesses":[1,2]}
```

Exact agreement. The independence is real: this arm computes `T^16(n)` with one
congruence-table lookup and one multiply-add per `n`, in Rust; the subject
iterates step by step in Python. Different language, different algorithm,
different author.

The two equality cases are **n = 1 and n = 2** — the elements of the trivial
cycle. `T` has period 2 there and 16 is even, so both are forced. Not a
curiosity; a structural consequence.

## 3. Paper 02 — every theorem, rechecked from the statements

`code/ot_paper02_recheck.py` re-derives Paper 02 from its own theorem
statements rather than from the subject's `tools/verify_math_claims.py`. Each
quantity is computed by routes that share no derivation:

| Route | What it assumes |
|---|---|
| **referee** | symbolic composition of `D(x)=x/2` and `U(x)=(3x+1)/2` on an affine form — **no theorem of the paper at all** |
| Theorem C | the closed form `b_w = Σ 2^{j_t−1} 3^{u−t}` |
| Theorem E | the upper-triangular matrix product `M_w = M_{σ_k}⋯M_{σ_1}` |
| engine tables | this arm's Rust `k`-step tables, derived by direct simulation |

The referee is the point. If a theorem were false, the referee is what would
disagree with it, because the referee never used it.

**All 13 checks pass at word length `k ≤ 16`:** 131,070 words, 260,100
concatenation pairs, 196,582 cylinder-transport cases.

| Check | Theorem |
|---|---|
| finite-word affine closure | A |
| correction recurrence `b_{wD}=b_w`, `b_{wU}=3b_w+2^{|w|}` | B |
| closed form of `b_w` | C |
| concatenation law `b_{wv}=3^{u(v)}b_w+2^{|w|}b_v` | D |
| matrix representation | E |
| order-extremal bounds `3^u−2^u ≤ b_w ≤ 2^{k−u}(3^u−2^u)` | F |
| extremes attained at `U^u D^{k−u}` and `D^{k−u} U^u` | §21 |
| width `W_{k,u}=(2^{k−u}−1)(3^u−2^u)` | §25 |
| parity word ↔ residue is a bijection | Paper 03 |
| residue cylinder is exactly the admissible domain | Paper 03 |
| `m_w` is an integer | Paper 03 |
| exact cylinder transport `T^k(r_w+2^k a)=m_w+3^u a` | Paper 03 |
| the all-`D` cylinder needs the `r_w+2^k` representative | the Paper 02/03 repair |

### Coverage this adds

- **Theorems B, D and E, and the §25 width formula, are not exercised by the
  subject's own regression suite at all.** `test_p02_p03` covers the affine
  data, residue coding and transport; `test_p02_extrema` covers Theorem F. The
  recurrence, the concatenation law, the matrix representation and the width
  formula were untested until now.
- The subject's suite enumerates words to `k ≤ 9`. This goes to `k ≤ 16`.
- The parity-word/residue bijection is checked in the **opposite direction**:
  enumerate all `2^k` residues, derive each one's word by simulation, confirm
  injectivity — verified for every `k` from 1 to 20. A bug in the
  word→residue formula cannot hide behind the same bug in the check.
- The `r_w = 0` boundary that the repair ledger is about is checked directly:
  the all-`D` cylinder does have canonical `r_w = 0`, the positive
  representative `r_w + 2^k` is admissible, and `T^k` of it is exactly 1.

**Correction, 2026-10-18 — the "1 to 20" above has no gate behind it.** No
committed code, now or in this file's history, runs the residue→word direction
to `k = 20`, and no log records it. What the gates actually check is narrower:
`ot_paper02_recheck.py` confirms word→residue **injectivity** for every `k ≤ 14`
(`counts.residue_max_k` in its log), and `ot_paper03_recheck.py` runs the
**opposite direction** — simulate every `n` in `[1, 4·2^k]`, read its word off
the dynamics, and require each of the `2^k` words exactly four times — for every
`k ≤ 11` (`P03_S9_level_k_atlas_partitions_the_positive_integers`). The
conclusion stands at those ranges, and the general statement is proved in Lean
(`LEAN-QUEUE.md`, item 3). The figure 20 was never true of this tree. Found
while writing the crystallized paper on Papers 01–04, which states the ranges
the logs hold.

## 4. Paper 06 — valuation language, all eight theorems

`code/ot_paper06_recheck.py`. Referee: direct iteration of the accelerated odd
map `S(n) = (3n+1)/2^{v₂(3n+1)}` on genuine odd integers, assuming no theorem of
the paper.

**All 19 checks pass**: every odd start below 20,001, twelve orbit prefixes each
— **120,000 admissible orbit prefixes** (86,863 on the contracting side, 33,137
expanding), 25,488 adjacent valuation swaps, 456 valuation multisets, 16,000
reverse recoveries.

| Check | Claim |
|---|---|
| run-length expansion is the genuine parity word, `\|E\|=K`, `u(E)=m` | A |
| accelerated affine closure `S^m(n)=(3^m n + B_κ)/2^K` **on real orbits** | B |
| the `B_j = 3B_{j−1} + 2^{K_{j−1}}` recurrence matches the closed form | C |
| exact log drift, verified as the equivalent rational identity | D |
| `2^K > 3^m ⟺ K/m > log₂3` | E |
| exactly one odd residue class mod `2^{j+1}` per valuation, and it is `3^{−1}(2^j−1)` | F |
| adjacent valuation swap `ΔB = 3^{m−i−1} 2^{K_{i−1}} (2^a − 2^b)` | G |
| closed reverse recovery `n₀ = (2^K n_m − B_κ)/3^m` | H |
| ascending order minimises, descending maximises the correction | §31 |
| the `θ_κ` descent threshold, both directions of the iff | §19 |
| uniform expansion when `2^K < 3^m` | §20 |
| stepwise reverse legality, not just the closed fraction | §35, §38 |
| terminal fiber `R_{2j}(1) = (4^j−1)/3`, odd | §39 |

### What this adds over the subject's own suite

The subject's `test_p06` checks **only** that the closed affine form agrees with
iterated `Fraction` arithmetic — for *formal* valuation tuples, `m ≤ 5`,
`κ ∈ 1..4`, and **only at `n = 1`**. It never checks admissibility, and it never
touches Theorems D through H, the §19 threshold, or §14.

Three things were worth doing that the subject's suite does not:

- **Admissibility.** Every orbit here is a real one: the valuation word is what
  `S` actually produced from a real odd `n`, not a tuple chosen on paper. A
  formal-tuple identity can hold while no integer realises the word.
- **The §14 bridge, verified across papers.** The claim `B_κ = b_{E(κ)}` — that
  the accelerated correction *is* the Paper 02 correction of the expanded parity
  word — is checked against the Paper 02 referee route. So the two papers'
  corrections are confirmed to be the same quantity, not merely analogous. This
  is the load-bearing joint between the two papers and it holds.
- **Theorem D without floating logarithms.** The paper states the drift in `ln`
  form. Rather than compare floats, the equivalent multiplicative identity is
  checked exactly over `ℚ`. Same content, no rounding.

### A float hazard recorded rather than glossed

Theorem E is exact over the integers. Deciding it with a `float` `log₂3` is not
safe in general, because `K/m` runs through the convergents of `log₂3`. The
check therefore decides it two ways — exact integers and 80-digit `Decimal` —
and additionally records what a naive float test would have said.

On `m ≤ 400` the float test happened to agree, and the closest ratio in range is
`K/m = 569/359` (a semiconvergent, mediant of `485/306` and `84/53`), whose
margin comfortably exceeds double epsilon. **That agreement is a fact about this
range, not a guarantee**, and it is recorded as such in `results.v1.json`. Push
`m` past 665 and the margin shrinks.

## 5. Paper 09 — the capstone, and the one place the engine meets the framework

`code/ot_paper09_recheck.py`. **All 13 checks pass** over 4,094 words to length
11 and 37,441 quotient-certificate cases.

Paper 09 §2 defines the coefficient stopping time

```
σ(n) = inf{ j ≥ 1 : T^j(n) < n }
```

which is **exactly** the quantity this arm's engine already measures for every
start it verifies, under the same map. §50 then identifies the frontier function

```
K(N) = min{ k : 𝔉_k(N) = ∅ } = max_{2 ≤ n ≤ N} σ(n)
```

So the archived `[3, 2^40]` run *already contained* Paper 09's `K(N)` — nobody had
to compute anything new to connect them.

### K(2^40) = 550

| | |
|---|---|
| `K(2^40)` | **550** |
| attained at | `n = 898,696,369,947` |
| over | 549,755,813,887 measured odd starts (even `n` have `σ = 1` by definition) |
| peak before first descent | `395,806,039,507,110,357,728` ≈ `4.404 × 10^8 · n` |
| cross-check | the Rust engine's claim, re-derived by an independent Python arbitrary-precision walk; both give 550, and `T^j(n) ≥ n` confirmed for every `j < 550` |

This is a **measurement, not a bound**. It says nothing about `K(N)` for larger
`N`, and Paper 09 §52 is explicit that no uniform `K` is there to be found —
`∀N ∃K(N)` does not commute to `∃K ∀N`, and the stronger form is incompatible
with observed unbounded stopping times. The number is offered as a data point in
the paper's own framework, at a scale the paper's prose does not reach.

Verified alongside it: Theorem B's hard-height characterisation
`H_w = Ω_w ∩ [1, h(w)]`, §8's claim that an expanding prefix imposes no height
bound at all, Theorem D's quotient threshold as an exact iff in both directions,
Theorem C's frontier-extinction equivalence, §56's monotonicity of the hard set,
and §44's stabilisation of canonical residues at `n` once `2^k > n`.

### §24's "finite boundary corrections", itemised exactly

Paper 09 §24 says the 938,413 strict-descent certificates are explained by Paper
05's 58,651 contracting residue classes "經 finite positive-domain 與
strict-equality corrections". That prose is now an exact accounting:

| | |
|---|---|
| contracting residue classes at `k = 16` | **58,651** (independently recomputed, and the Paper 05 binomial counts for `k = 8, 12, 16, 20` all confirmed) |
| starts in a contracting class on `[1, 2^20)` | **938,415** — 16 per class, less one, because `n = 0` lies outside the domain |
| strict descents | **938,413** |
| shortfall | **exactly 2** |
| itemised | `n = 1` and `n = 2` — both meet `T^16(n) = n`, equality rather than strict descent |
| ascents inside a contracting class | **0** |

So the "corrections" are two named integers and one excluded residue, and
nothing else. The class-based count and the certificate count are now reconciled
term by term rather than approximately.

## 6. Paper 07 — the generalization, and a floating floor worth attacking

`code/ot_paper07_recheck.py`. **All 27 checks pass** across **24 `(m, r)`
parameter pairs** (`m ∈ {1,3,5,7,9,11}`, `r ∈ {1,3,5,7}`), 73,248 transport
cases and 30,752 concatenation pairs.

Theorems A–D and §5, §8, §9, §12, §15, §17–§22, §25, §33, §37, §46, §47 all hold.
The subject's `test_p07` covers the affine data, residue coding and transport for
`m ∈ {1,3,5,7,9}`, `r ∈ {1,3,5}`, `k ≤ 7`. It does **not** touch the matrix
representation, the concatenation law, the closed geometric-sum bounds, the §21
threshold, §22, Theorems E–H, §33's linearity in `r`, §46's width, or §47's
order-uniform threshold. Those are all now checked.

### The `m = 1` repair, verified on its own terms

The repair ledger records that Paper 07's theorem summary used `ln m` without
restricting `m > 1`, and now states the logarithmic forms for odd `m > 1` while
recording `P_k(1) = 1` separately.

Both halves check out — and the recheck is written so that it *could* have caught
a residual singularity: the §17/§18 bounds are stated with an `(m−2)` denominator,
but this recheck evaluates the underlying geometric sum
`Σ 2^t m^{u−1−t}` **directly, never dividing**, and then confirms
`geo·(m−2) = m^u − 2^u` separately. So `m = 1` is reached by the same code path as
every other `m`, with no special case and no division by anything that could
vanish. `b_min = r(2^u − 1)` at `m = 1` confirmed, and `P_k(1) = 1` exactly.

### Theorems E–H, and the hazard in the paper's own counting code

Theorems E and F are stated with `α_m = ln2/ln m` and a floor. `α_m` is
irrational for odd `m > 1` — the paper's §25 proof is one line and correct — so
the floor is well defined. But **the subject's own p05 counting code computes that
floor in double precision**, and `k·α_m` runs arbitrarily close to integers.

This recheck takes the exact integer predicate `m^u < 2^k` as the reference and
reports every `k` where the float disagrees. Over `m ∈ {3,5,7,9,11,13}` and
`k ≤ 3000`: **no disagreements**.

Agreement over a range is weak on its own, so the margin was measured too, in
60-digit arithmetic:

| `m` | closest `k·α_m` comes to an integer | at `k` | double-error bound over the range | safety factor |
|---|---|---|---|---|
| 3 | `3.974 × 10⁻⁵` | **1054** | `4.203 × 10⁻¹³` | `9.45 × 10⁷` |

`k = 1054` is not a coincidence: it is the convergent denominator of `ln2/ln3`
(`665/1054`), exactly where a Diophantine near-miss is expected. The float floor
is therefore safe **for a reason**, not by luck — and the reason comes with a
number. Push `k` far enough that the Diophantine margin `~1/k` drops below
`k·2⁻⁵³` and it would stop being safe; that is around `k ~ 10^8`, well outside
anything the series computes.

Theorems G and H measured on the exact boundary:

| `m` | `P_10` | `P_40` | `P_160` | `P_640` |
|---|---|---|---|---|
| 1 | 1 | 1 | 1 | 1 |
| 3 | 0.828 | 0.960 | 0.99944 | 0.99999999998 |
| 5 | 0.377 | 0.215 | 0.0343 | 0.000213 |
| 7 | 0.172 | 0.0403 | 9.15×10⁻⁵ | 8.90×10⁻¹⁴ |

`P_k(3) → 1`, `P_k(5), P_k(7) → 0`, and `α_m = 1/2` exactly at `m = 4`. §37's
claim that the one-step valuation density `2^{−j}` is independent of `(m, r)` for
odd parameters is confirmed across all 20 pairs tested.

## 7. Paper 03 — the same residue, derived twice

`code/ot_paper03_recheck.py`. **All 13 checks pass** at `k ≤ 13`: 16,382 words
with `r_w` derived twice, 114,661 transport cases.

### Why this needed its own recheck

Four of Paper 03's statements were already confirmed as a by-product of §3 above.
But they were confirmed *using the closed congruence* `r_w ≡ −b_w 3^{−u} (mod 2^k)`
— which is exactly the shortcut Paper 03 §11 warns against resting on:

> 若沒有另外証明 finite parity coding 的唯一性，直接從「最終整數」跳到「每個
> intermediate parity branch 都正確」會留下討論缺口。

So `r_w` is derived a **second time**, by the §6/§7/§28 refinement induction: start
from `r_D = 0`, `r_U = 1`, and split each cylinder into `r_w` and `r_w + 2^k`
according to the parity of `m_w`. That route **never touches** `b_w 3^{−u}`.

The two derivations agree on all 16,382 words. That is what makes the closed
congruence a *result* rather than an assumption — and it is the check the paper's
own repair note is about.

The drill confirms both routes are load-bearing: perturbing the refinement
parity, the induction's base case, or the child offset all break the agreement,
and so does inverting the congruence's exponent. Neither route is decorative.

### Also verified

| Check | Claim |
|---|---|
| the cylinder is exactly the admissible domain | A |
| word ↔ residue bijection, and the level-`k` partition | B |
| the closed residue formula, against the induction | C |
| exact cylinder transport | D |
| local identity trivialization `ψ_w ∘ T^k ∘ φ_w^{-1} = id` | E |
| exact recovery | F |
| the two children are exactly `{r_w, r_w + 2^k}` | §7 |
| the level-`k` atlas partitions the positive integers | §9, §26 |
| faithfulness: `F_w` is injective on its cylinder | §19 |
| the next branch is decided by the quotient bit alone | §29 |
| nested residues form an inverse system | §32 |
| all five worked examples, against the paper's own numbers | §20–§24 |
| target charts overlap — with a witness | §27 |

The five worked examples match exactly as stated: `r_D=0, m_D=0`; `r_U=1, m_U=2`;
`r_{UD}=1, m=1`; `r_{DU}=2, m=2`; and `UUDD` with `k=4, u=2, b=5, r=3, m=2`,
including the explicit orbit `3 → 5 → 8 → 4 → 2`.

§27 is another non-claim given a witness rather than a nod: source charts
partition, but target charts need not, and `DDDD` and `DDDU` both reach 2 at
depth 4.

### One attribution fix

Three of the Paper 03 mutations initially registered as "caught by crashing"
rather than by a named check: a wrong residue makes `m_w` non-integral, and an
assertion fired before any check could report. A crash is a detection, but a weak
one — it says something broke, not what. The integrality failure is now a named
exception that the comparison reports as a disagreement, so all three attribute
properly. Across the whole drill only one mutation still detects by crashing, and
that one legitimately: inverting `α` to `ln3/ln2` makes `1 − α` negative, and
there is no meaningful check to route `ln` of a negative through.

## 8. Paper 08 — the breakage ladder, one witness per rung

`code/ot_paper08_recheck.py`. **All 19 checks pass.**

### Correcting an earlier judgement of mine

An earlier version of this report wrote Paper 08 off as out of instrument range,
because it is about general commutative rings, zero divisors, noncommutative
algebras, Möbius maps and higher-degree polynomials. **That was too quick.**

A *structural breakage theorem* does not need a general proof to be tested. It
needs an explicit **witness** that the property really does fail there, and
confirmation that the properties *above* it in the ladder really do survive. Both
are finite, and both are squarely this instrument's range.

What still needs a proof assistant is only the universally quantified form — "for
*every* commutative ring and *every* ideal" — and that is what stays in
`LEAN-QUEUE.md`, whose Paper 08 entry has shrunk accordingly.

### One witness per rung of §43's ladder

| Level | What breaks | Witness |
|---|---|---|
| 1 | unique residue coding | `ℤ/6ℤ`, multiplier 2: `2x ≡ 2` has **two** solutions `{1,4}`; `2x ≡ 1` has **none** |
| 2 | faithful recovery | `2·1 ≡ 2·4 ≡ 2 (mod 6)` while `1 ≠ 4` |
| 3 | counts fix the leading drift | `A=[[1,1],[0,1]]`, `B=[[1,0],[1,1]]`: `AB=[[2,1],[1,1]] ≠ [[1,1],[1,2]]=BA`, identical branch counts |
| 4 | arithmetic-progression transport | Möbius `x ↦ (x+1)/x` on `1+a`: image `2, 3/2, 4/3, 5/4`, differences `−1/2, −1/6, −1/12` |
| 5 | fixed-degree closure | `x²+1` iterates have degree `2, 4, 8, 16` |

Every stated number in §10, §12, §26 and §37 matches exactly.

**Correction, 2026-10-18 — Theorem A's count law was not checked by this run.**
`P08_ThmA_commutative_affine_closure_counts_fix_A_and_D` was meant to confirm
that `A_w` and `D_w` depend only on branch counts, by comparing each word with
"one alternative ordering". The alternative was the first item of
`itertools.permutations(combo)` — which is `combo` itself — so every word was
compared with itself and the check could not fail. The drill never noticed,
because no planted defect was aimed at it. Repaired: each word is now compared
with its sorted rearrangement, a different ordering for 6,359 of the 6,678 words,
and agreement on all of them is exactly count-determination
(`counts.words_compared_with_a_different_ordering` in the log). A new drill
defect, `K08`, makes the leading product order-dependent; against the old check
it survived — Theorem A stayed green and only the `UUDD` and `ℤ/6ℤ` spot values
noticed — and against the repaired one it is caught by the check named for it.
The theorem itself was never in doubt: its universal form is proved in Lean
(`Aw_perm`, `Dw_perm`, `LEAN-QUEUE.md` item 7). What was wrong was this run's
claim to have checked it. Found while writing the crystallized paper on Papers
07–08.

### Each rung checked in both directions

The paper's real content is not "it breaks" but *what survives when it breaks*, so
both halves are checked:

- **§11** — at the very same `ℤ/6ℤ` witness where residue uniqueness fails, the
  affine closure is **untouched**: the operator still composes by §3's rule and
  §4's mother formula still gives `B_w`. "Closure survives while unique residue
  coding fails" is verified at one witness, not two.
- **§14** — the two failure modes are kept apart with a witness each. `2` in `ℤ`
  is a **non-unit but injective**; `2` in `ℤ/6ℤ` is **both**. So "non-unit" and
  "zero divisor" are confirmed to be genuinely different conditions, controlling
  residue uniqueness and exact recovery respectively.
- **§31** — dimension is confirmed **not** to be the breakage point. Commuting
  (here diagonal) matrix families keep the count law: the product is
  order-independent, and each eigendirection carries a scalar-like multiplier
  exactly as stated. The boundary really is noncommutativity, not `dim > 1`.

Theorems B and C are also checked exhaustively over `ℤ/nℤ` for `n ≤ 40`: a unit
multiplier gives exactly one solution for **every** right-hand side, a non-unit
admits both a right-hand side with none and one with several, and "regular
multiplier" and "injective" are confirmed equivalent on every `(n, A)` pair.

### The §32 repair, with a minimal witness

The repair ledger records that Paper 08's Möbius subsection wrote `ad − bc ≠ 0`
without stating the coefficient domain, and that over a general commutative ring
the condition must be `ad − bc ∈ R^×`.

That correction is exactly the kind of thing a witness settles:

```
ℤ/4ℤ,  M = [[0, 1], [2, 0]],  det = 2
    determinant is nonzero      ✓
    determinant is a unit       ✗
    matrix is invertible        ✗
```

`det ≠ 0` holds and invertibility still fails — so the unrepaired condition would
have admitted this matrix. The repaired one does not.

### Collatz's own position

§46 claims Collatz sits at Level 0 of the ladder. All six conditions were checked
rather than assumed: scalar, affine, commutative, `3^u ∈ (ℤ/2^kℤ)^×` for every
`k ≤ 8` and every `u ≤ k`, `3^u` regular, and the state domain ordered.

Which is the paper's point, and worth restating because it is the one conclusion
of this whole series that bears on where the difficulty actually lives: **Collatz
is not hard because its local operator is complicated.** Its local arithmetic sits
in the cleanest interior of the RCOT domain, and can be trivialised to the
identity. The difficulty is entirely in which chart comes next.

### One more drill defect of mine

`K07` — the mutation aimed at the §32 witness search — made that search
pathologically slow rather than wrong. The drill's `run()` had **no timeout
handler** (only the engine's separate drill did), so the `TimeoutExpired` escaped
and took the whole run with it, discarding every verdict already earned. Fixed:
timeouts are caught, reported as `<timed out>`, and counted as a detection. The
per-target budget also came down from 900s to 300s, since the slowest legitimate
baseline runs well under a minute and the old figure only ever gave a runaway
mutant more rope. The same pass removed a redundant `n⁴` scan in the recheck whose
result was computed and never used.

## 9. Paper 01 — the ledger's arithmetic, and the bibliography

`code/ot_paper01_recheck.py`. **All 12 checks pass.**

### Correcting a second judgement of mine

An earlier version of this report said Paper 01's content is "bibliographic
rather than arithmetic — a different instrument again: this arm can check
numbers, not literature." **Wrong twice over.**

**Citations are externally checkable.** An arXiv identifier either resolves to a
record with the stated title, authors and date, or it does not. A DOI either
resolves to the stated journal, volume and article, or it does not. That is an
external anchor of exactly the kind this tree values most — the expectations are
not authored here.

**And Paper 01 is not only bibliographic.** Its Claim Ledger sorts old results
into `T`/`E`/`C`/`H`/`N`/`S` by evidence strength, and every `T` entry is a
concrete arithmetic statement. A merely heuristic claim filed as `T` would be
precisely the defect the ledger exists to prevent, so those labels are worth
checking.

### The ledger's arithmetic

| Check | Ledger entry |
|---|---|
| `n` has a legal odd predecessor iff `n ≡ 4 (mod 6)` | §4.1, `T` |
| that class has natural density `1/6` | §4.2, `T` |
| unique odd-core decomposition `n = 2^{v₂(n)} · oddcore(n)` | §4.3, `T` |
| coverage of `ℤ_{>0}` reduces to coverage of the odd integers | §4.3, `E` |
| a trajectory reaches 1 iff it meets a power of two | §5, `E` |
| exactly `v₂(n)` halvings precede the odd core | §6.1, `T` |
| binary tree rotation preserves the node set | the rotation no-go, `N` |
| the Barina milestone ladder is monotone and ends at `2^71` | §7.1, `C` |
| the GGM threshold `q < p^{p/(p−1)}` is exactly `q < 4` at `p = 2` | the Paper 07 calibration |

Each was checked against a brute-force referee rather than against the paper's
own reasoning — the odd-predecessor rule, for instance, against an actual search
for an odd `m` with `3m + 1 = n`. The rotation no-go is checked on concrete trees
by comparing node multisets before and after, rather than argued.

### The bibliography, against the sources

Every load-bearing reference was fetched and compared, with the records
snapshotted under `../data/external/bibliography/` and digested on every run:

| Reference | Verified |
|---|---|
| Rozier, arXiv:1805.00133 | title, author, *Integers* 19 (2019) A8 |
| Tao, arXiv:1909.03562 | title, author, *Forum Math. Pi* 10 (2022) |
| Gonçalves–Greenfeld–Madrid, arXiv:2111.06170 | title, all three authors |
| Angeltveit, arXiv:2602.10466 | title, author, 2026-02-11 |
| Niu, arXiv:2605.13886 | title, author, 2026-05-11 |
| Applegate–Lagarias, arXiv:math/0411140 | title, authors, *J. Number Theory* 117 (2006) |
| Barina 2025, doi:10.1007/s11227-025-07337-0 | title, author, *J. Supercomputing* **81**:810, 2025-05-02 |
| Barina project page | states convergence verified below `2075 × 2^60 ≈ 2^71.02` |

All match. The package's own `EXTERNAL_REFERENCE_AUDIT.md` is therefore
independently confirmed on every item it spot-checked.

### And it corrected *this* tree

This is the part worth reporting plainly, because verifying someone else's work
turned up an error in mine.

Until 2026-08-14 this tree's charter and README said the published frontier was
**"at least `2^68`"**, citing Barina 2021. The current figure is all `n` below
`2075 × 2^60 ≈ 2^71.02`, from Barina 2025.

The old statement was *literally true* — `2^71` is at least `2^68` — which is
exactly why it survived unexamined. But it understated the frontier by three
doublings and cited a superseded milestone, in the one place this tree insists on
being precise: how far below the real frontier its own `2^40` sits. It is now
corrected in `CHARTER.md`, `README.md` and `RUN-001-T40.md`, each carrying a note
of what it previously said.

Neo.K's reference audit had the current figure all along. The error was mine, and
the only reason it surfaced is that his paper was checked rather than assumed.

## 10. Paper 04 — bidirectional transport, never machine-checked before

`code/ot_paper04_recheck.py`. **All 21 checks pass** at `k ≤ 10`: 22,506
transport triples and 112,530 negative controls.

**The subject's regression suite contains no Paper 04 test.** Its groups are
`p02_p03`, `p02_extrema`, `p05`, `p06`, `p07` and `p09`. Every theorem below was
machine-checked here for the first time.

| Check | Claim |
|---|---|
| bidirectional residue transport `r_w + 2^kℤ ↔ m_w + 3^uℤ` | A |
| exact inverse `x = r_w + 2^k(y − m_w)/3^u` | B |
| target legality `y ≡ m_w (mod 3^u)` | C |
| quotient conservation `(x−r_w)/2^k = (y−m_w)/3^u` | D |
| accelerated fiber legality `R_κ(t)` iff `2^κ t ≡ 1 (mod 3)` | E |
| terminal fiber `R_{2j}(1) = (4^j−1)/3` | F |
| the division-free relation `3^u(x−r_w) = 2^k(y−m_w)` | §8 |
| `a_min(w)` and the positive-domain bijection | §9, §10 |
| the `w = U` worked example: `r_U=1`, `m_U=2`, `1+2a ↔ 2+3a` | §11 |
| `T^{-1}(y) = {2y} ∪ {(2y−1)/3 : y ≡ 2 mod 3}`, exactly | §12 |
| `y_orig ≡ 4 (mod 6)` and `y_mod ≡ 2 (mod 3)` are the same constraint | §13 |
| the mod-3 classification of admissible κ, all three cases | §22 |
| the accelerated image never hits a multiple of 3 | §23 |
| `M_j = 1, 5, 21, 85, 341`, `S(M_j)=1`, `v₂(3M_j+1)=2j` | §24, §25 |
| `5 = R_4(1)`, trajectory `5→16→8→4→2→1` | §26 |
| odd-core decomposition and 2-ray partition | §17 |
| `n` converges iff its odd core does | §18 |
| the §38 certificate accepts every legal triple | §38 |
| the §38 certificate **rejects** perturbed triples | §38 |

Two of these deserve their own note.

### The certificate had to be checked in the direction that matters

§38 offers a three-condition bidirectional certificate: source congruence, target
congruence, and transport consistency. Confirming it accepts legal triples is the
easy half and proves almost nothing — **a certificate that accepts everything
certifies nothing.** So 112,530 deliberately perturbed triples were generated
(shifting `x` by 1, by `2^k`, `y` by 1, by `3^u`, and both together) and every one
was required to be refused. All were.

The drill confirms this is load-bearing: dropping the transport-consistency
condition and keeping only the two congruences leaves the accepting half perfectly
green, and is caught **only** by the rejecting half.

### A non-claim, given an actual witness

§33 insists that local bijectivity does **not** give global injectivity. That is a
claim that something *exists*, so asserting it would be the wrong response. An
explicit cross-chart merge was searched for and found:

```
w = "D", source 4  ->  2
v = "U", source 1  ->  2
```

Two different charts carrying two different sources to the same target in one step
each — minimal, and exactly what §33 says must be possible. Each chart is still
injective on its own cylinder; that is the distinction the paper draws, and it now
has a witness rather than a sentence.

### Another no-op mutation, caught by the drill

The first attempt at perturbing Theorem F used `(4^j + 1)/3` instead of
`(4^j − 1)/3`. That is a **no-op**: `4^j + 1 ≡ 2 (mod 3)`, so floor division
returns `(4^j − 1)/3` unchanged. Third mutation in this drill defeated by an
arithmetic identity rather than by the checks — after `3^u ≤ 2^k` versus
`3^u < 2^k` in Paper 09, and `<` versus `<=` in Paper 07. Re-aimed at the family
index, it is caught by three checks at once.

## 11. Paper 05's KL constant, and a finding

`code/ot_paper05_kl_recheck.py`. The last remaining numeric claim in the six
finite groups.

`validation.json` records `KL = 0.03468818523201744`, and the subject's suite
asserts it to within `1e-14` of `α·ln(α/0.5) + (1−α)·ln((1−α)/0.5)` — where that
expression is evaluated by the same float code the literal came from. **That
assertion cannot fail.** It compares a double against itself with a tolerance
eleven orders of magnitude wider than the quantity's precision.

Two things were done instead.

### The digits, against the real value

Recomputed at 60 digits:

```
true value  0.034688185232017459384287451545…
published   0.03468818523201744
```

**Finding.** The published literal is exactly what the stated float expression
emits — so it is not a typo — but it is **2.79 ULP from the real value**, and it
is not the nearest double. The nearest double is `0.03468818523201746`. The 17th
significant digit reads `…744` where the true value rounds to `…746`; the first 16
are correct.

This is a precision-reporting defect, not a mathematical one. Nothing in the
series depends on the 17th digit, and `α` itself *is* correctly rounded. But it is
the kind of thing that only shows up when the constant is compared against the
real number rather than against its own float computation.

### The constant's role, on exact binomial tails

The digits are the small half. `D` is the Kullback–Leibler divergence of
Bernoulli(α) from Bernoulli(1/2), and the reason it appears in Paper 05 is that it
governs how fast the non-contracting fraction decays. That has consequences, and
consequences can be measured:

| `k` | `1 − P_k` (exact) | `exp(−kD)` | `−(ln(1−P_k) + kD) − ½ln k` |
|---|---|---|---|
| 50 | 3.245×10⁻² | 1.765×10⁻¹ | −0.26 |
| 500 | 1.909×10⁻⁹ | 2.935×10⁻⁸ | −0.37 |
| 2000 | 3.046×10⁻³² | 7.417×10⁻³¹ | −0.61 |
| 8000 | 4.977×10⁻¹²³ | 3.026×10⁻¹²¹ | −0.39 |

The Chernoff bound holds at every `k`. The sharp column is the last one: if `D`
were the wrong rate, it would drift **linearly** in `k` instead of staying inside
a fixed window. It stays between −0.65 and −0.06 across a 160-fold range of `k`.
The residual wobble is expected — the tail starts at `u_max + 1` and the
fractional part of `αk` oscillates — so boundedness is the claim, not smoothness.

### How sharp that is, stated rather than implied

A relative error `ε` in `D` displaces that column by `ε·D·k`, so it clears the
`O(1)` window only once `k ≳ 2/(ε·D)`. At `k = 8000` that resolves about **0.72%**.
Measured: a 1% wrong `D` is rejected; **a 0.1% wrong `D` is not** — it gives
`−0.663`, still inside the window, exactly as the formula predicts. So the rate
test pins `D` to about one part in a hundred, and the 60-digit comparison is what
pins it further. Both are recorded; neither is asked to do the other's job.

### What the drill did to this file

This recheck was the most heavily corrected of the five, and every correction came
from the drill rather than from reading it again:

- The relative-error check divided by `D` **without guarding its sign**, so a
  mutation that made `D` negative passed it — a negative ratio is less than
  `1e-15`. Guarded.
- The Chernoff bound carries several-fold headroom, so it could not notice a
  one-step shift in the class boundary. A direct check was added, pinning the
  exact boundary against the independent floating route `floor(k·ln2/ln3)`.
- Nor could it notice a tail that double-counts one term. A complementarity check
  was added: head and tail must sum to exactly `2^k`.
- That new complementarity check then **re-derived the tail inline**, so mutating
  the tail function left it untouched — a check that did not exercise the code it
  was named for. Routed through the function.

The gate also had to learn a distinction it did not have: **a finding about the
subject is not the instrument breaking.** The KL ULP result is recorded under
`subject_findings` and does not set the run's exit status, because otherwise a
real defect in the subject would be indistinguishable from a broken checker — and
`build_results.py` would refuse to archive the very finding worth keeping.

## 12. All nine rechecks were drilled

A recheck that passed everything is worth what it could have caught.
`code/ot_recheck_drill.py` perturbs each asserted formula by one term and
requires the run to fail **the check named for that formula** — not merely some
check.

Paper 02 target:

| Planted defect | Checks that failed |
|---|---|
| Theorem C exponent `3^{u−t+1}` | `ThmC` only |
| `M_U = [[3,2],[0,2]]` | `ThmE` only |
| recurrence adds `2^k` not `2^{|w|}` | `ThmB` only |
| concatenation uses `2^{|v|}` not `2^{|w|}` | `ThmD` only |
| Theorem F lower bound off by one | `ThmF` only |
| §25 width drops the `−1` | `S25` only |
| §21 argmin/argmax swapped | `S21` only |
| residue uses `3^{+u}` not `3^{−u}` | all four Paper 03 checks |
| **the referee itself**: `U` injects `2·Dn` | eight checks cascade |
| control: comment added | none |

Paper 06 target:

| Planted defect | Checks that failed |
|---|---|
| Theorem C exponent `3^{m−i+1}` | seven checks cascade — `B_closed` is what everything references |
| recurrence uses `2^{K_j}` not `2^{K_{j−1}}` | recurrence check only |
| expansion emits `D^κ` not `D^{κ−1}` | Theorem A and the §14 bridge |
| Theorem G exponent off by one | Theorem G only |
| §19 threshold drops the `+1` | §19 only |
| Theorem H divides by `3^{m−1}` | Theorem H only |
| reverse step uses `2^κ t + 1` | stepwise legality and the terminal fiber |
| density counted mod `2^j` not `2^{j+1}` | Theorem F residue count only |
| mean-valuation partial sum drops the `+2` | that series check only |
| **the referee itself**: `S` divides by `2^{κ−1}` | seven checks cascade |
| control: comment added | none |

Paper 09 target:

| Planted defect | Checks that failed |
|---|---|
| hard height takes the max over contracting prefixes, not the min | Theorem B only |
| hard height also admits expanding prefixes | Theorem B only |
| quotient threshold uses `≥` instead of `>` | Theorem D only |
| a class counts as contracting one power of two too early | the 58,651 count and the §24 accounting |
| Paper 05 class count sums to `m` instead of `m+1` | the binomial counts only |
| contraction exponent uses `log3/log2` | the binomial counts only |
| `σ` counts from 0 instead of 1 | **the σ anchor only** — see below |
| **the referee itself**: `T` halves odd values too | nine checks cascade |
| control: comment added | none |

Paper 07 target: all nine planted defects caught by the check named for each —
the Theorem B exponent, the §5 recurrence, the `M_U` matrix entry, the §17
geometric sum, §33's factor of `r`, the §21 threshold, the Theorem C residue
sign, §47 using the minimum correction where the maximum is required, and the
referee itself (which cascades into thirteen checks).

**68 defects planted across the nine rechecks, 68 caught, 9 controls
undisturbed.** One was caught by crashing rather than by a named check, which is
recorded as such rather than counted as a clean hit. *(Since 2026-10-18 there are
69: `K08` was added with the repair of Paper 08's Theorem A check — see the
correction at the end of §8.)*

### A gap the drill found, and what was done about it

The `σ`-off-by-one mutation initially **survived every check**. That was correct
behaviour from the checks and a real hole in the design: the frontier check, the
`K(N)` identity and the monotonicity check all compare `σ` only against *itself*,
so a uniform shift moves both sides and leaves every one of them green.

The fix is a separate anchor that pins `σ`'s absolute indexing against values
derived independently in `collatz_ref.py` — `σ(3)=4`, `σ(7)=7`, `σ(27)=59`,
`σ(703)=81`, `σ(10087)=105`. With that in place the mutation is caught, and
caught by exactly one check. This is the same lesson as elsewhere in this tree:
a quantity compared only to itself is not pinned by anything.

Two other things the drill corrected before they shipped. One planted "defect"
was a no-op — `3^u ≤ 2^k` and `3^u < 2^k` are the same predicate because `3^u` is
odd — so it had to be re-aimed at the exponent to be a defect at all. And the
Paper 09 baseline failed at first because a mutant runs from a scratch directory
and could not find the archived `coverage.json`; the check refused rather than
skipping, which is right, so the drill now passes the tree root explicitly
instead of the check being softened.

Cascades are worth reading correctly. Breaking any referee brings down most of
that paper's checks — that is the point of having one. The Paper 06 Theorem C
mutation cascades because `B_closed` is the single claimed formula the other
checks are written against; the recurrence check is what isolates it, and it
fired alone when the recurrence itself was perturbed.

### One honest insensitivity

Breaking the referee's `+1` injection did **not** break Theorem A or Theorem D.

- Theorem A only asserts the slope `3^u` and denominator `2^k`, which the
  mutation left alone. Correct by construction.
- Theorem D is **structurally insensitive to the injection constant**: the
  concatenation law `b_{wv}=3^{u(v)}b_w+2^{|w|}b_v` holds across the whole
  `(mx+r)` family and does not pin `r`. This is a true property of the theorem,
  not a hole in the check — but it means **Theorem D alone cannot detect a wrong
  injection constant**, and should not be leaned on for that.

## 13. Where this stands

| Group | Cases claimed | Status |
|---|---|---|
| `p02_p03_affine_residue_transport` | 4,079 | **re-derived**, and extended to `k ≤ 16` |
| `p02_correction_extrema` | 54 | **re-derived** (Theorem F, §21, §25) |
| `p05_binomial_and_k16_benchmark` | — | **re-derived** — block counts, class counts, and §24 reconciled term by term |
| `p06_accelerated_affine_formula` | 1,364 | **re-derived**, on real orbits rather than formal tuples |
| `p09_hard_height` | 8,167 | **re-derived**, plus Theorems B–D, §8, §44, §50, §56 |
| `p07_generalized_mxr` | 11,325 | **re-derived**, over 24 `(m, r)` pairs, plus Theorems E–H |

**All six groups re-derived**, each from the paper's own theorem statements
rather than by re-running the subject's suite, and each drilled to confirm the
checks could have failed.

Remaining, in order of what this arm can usefully do next:

- **Hard-Zeta's `n ≥ 2` stopping domain** — that `E_k^C = ⊔_{|w|=k} (H_w ∩ 2,∞))`
  is a genuine disjoint partition of the hard set with `n = 1` excluded is a finite
  statement per `k`, and it connects directly to the `H_w` and `σ` machinery
  already built for Paper 09. **This is the next non-Lean task.**
- **Paper 04 is now complete** (§7 above), and it was the largest untested gap in
  the series: the subject's suite had no Paper 04 test at all.
- **Paper 03 is now complete** (§7 above), with `r_w` derived independently twice.
- **Paper 08 is now complete** (§8 above), with one explicit witness per rung of
  its ladder and each rung checked in both directions. Only its universally
  quantified forms remain, in `LEAN-QUEUE.md`.
- **Paper 01 is now complete** (§9 above) — both halves of it, and it corrected
  this tree's own understated frontier along the way.

**Every core paper of the series has now been independently rechecked.** What
remains is the Hard-Zeta research program: its `n ≥ 2` stopping-domain correction
is finite per `k` and checkable here; its invariant-measure route is
`∀`-quantified over function spaces and is not.
- **Hard-Zeta's invariant-measure route** is `∀`-quantified over function spaces,
  which this instrument cannot address at all. Those are collected, scoped and ordered in
  [`LEAN-QUEUE.md`, and deliberately not started: Lean is
  available but the hardware for a mathlib-backed development comes later.

Nothing in this report bears on the Collatz conjecture. Paper 09 §62 lists its
own non-claims, and they stand: no uniform extinction depth, no closed bound on
`K(N)`, no exclusion of an integer-anchored infinite hard branch, and no
inference from survivor density to emptiness. `K(2^40) = 550` is one value of a
function the paper defines; the paper's whole point is that no finite number of
such values closes the quantifier gap.