---
title: "Where the local theory of the Collatz map holds: the odd (m, r) family, a phase boundary at m = 4, and a ladder of algebraic breakage"
subtitle: "Every statement of the local affine atlas holds verbatim for n/2 and (mn+r)/2 with m and r odd; the binomial law turns over at m = 4; and each algebraic property the theory leans on is removed in turn, with a witness for what breaks and a check of what survives"
author:
- "Aletheia — the series' documents; model: ChatGPT, GPT series"
- "Neo.K — AMRAL Research Lab"
- "墜衡 (Zhuì Héng) — AMRAL Research Lab, verification; model: Claude, Opus series"
date: 2026-10-18
version: "0.1"
standard: "1"
headline_problem: "Collatz conjecture"
evidence:
branch: agent/collatz-verification-zhuiheng
commit: "a2c25aa757c0704bc110458684ef3d459cb3d9e0"
dir: collatz-verification-zhuiheng
sources: "data/gate-logs/ot-paper07-recheck.json, data/gate-logs/ot-paper08-recheck.json, data/gate-logs/ot-recheck-drill.json, data/paper-figures.json, data/gate-logs/suite-totals.json, data/results.v1.json"
abstract: |
The Collatz conjecture is open, and nothing here bears on it. Its local theory — every finite parity
word acts as one exact affine map on one residue class, in coordinates where the dynamics is the
identity — is shown here not to depend on the numbers 3 and 1. For the map $n/2$ or $(mn+r)/2$ with
$m$ and $r$ positive and odd, every word of length $k$ with $u$ odd steps acts as
$x \mapsto (m^u x + b_w)/2^k$ on exactly one class modulo $2^k$, carries it onto a progression of
difference $m^u$, and splits into a skeleton fixed by the counts and a correction fixed by the order;
$r$ only scales the correction. The binomial count of contracting classes then turns over at $m = 4$:
their proportion tends to one for $m = 3$, is one for $m = 1$, and tends to zero for every odd
$m \ge 5$.
The paper then removes, one at a time, each algebraic property that theory uses — units modulo the
quotient, regular multipliers, an order, commutativity, affinity, degree one — and for each rung gives
an explicit witness that the property fails there together with a check that what lies above it
survives, including a two-by-two matrix over $\mathbb{Z}/4$ that witnesses why a Möbius condition had to be
repaired. The Collatz map sits at the cleanest rung: its local arithmetic is as simple as this kind of
arithmetic gets, so its difficulty lies in which chart comes next. Along the way three things are set
right rather than restated: the series' two derivations of the critical value 4 are one fact in two
coordinates, not independent confirmation; a floating-point floor in its counting code is safe for a
reason, with its closest call at a convergent of $\ln 2/\ln 3$; and this line's own finite check of the
count law at the bottom of the ladder compared every word with itself, and is repaired.
keywords: [Collatz conjecture, generalized Collatz maps, residue classes, phase boundary, algebraic structure, formal verification]
---
> **Status of this document.** Preprint, version 0.1: complete enough to stand in public, and not
> final; a later version may revise it. Not prepared for journal submission. Section 9 records who
> did which part, including the parts this line did not do.
# 0. What is claimed, and what is not
Six kinds of statement are kept apart and never merged; the distinction is not presentational,
it is the content.
| label | meaning |
| --- | --- |
| `COMPUTED_HERE` | recomputed in this line with independently written code, never by running the programme's own scripts |
| `DERIVED_FROM_VERIFIED_INPUTS` | follows from quantities this line already computed |
| `CITED_THEOREM` | a published result, cited and checked as a citation |
| `INHERITED` | taken from the programme's documents and never verified here; every use is marked |
| `UNMEASURED` | well posed, and not established here |
| `FAILED` | attempted and refused |
In particular `PASS` and `PASS by cited theorem` are **different verdicts** and are never written
as one; no result in this paper rests on a cited theorem.
**Not claimed anywhere in this paper:** the Collatz conjecture, or any statement about the orbits of
any map in the family; that the phase boundary at $m = 4$ for the proportion of contracting classes
decides the behaviour of orbits on either side of it; that the family's local simplicity makes the
global problem tractable for any $(m, r)$; that a system failing a rung of the ladder cannot be
analysed; and novelty of the elementary statements, most of which are classical in other notation.
**Inherited:** one statement, used once and marked there (§3): the series' report of the condition
under which a published almost-all theorem for generalized Collatz maps holds. That paper's title and
authors were checked against its record; the condition itself was not.
Where the other labels sit: the theorems of §§2–5 are proved in the text and checked, and those of
§§2 and 5, the projective rung apart, are also formalized in their universal form; the tables are `COMPUTED_HERE`; the
convergent behind the float floor's closest call is `DERIVED_FROM_VERIFIED_INPUTS`; this line's
original finite check of the count law of §5 is `FAILED` as evidence and replaced (§7); and whether
the projective rung admits a formal statement of what it loses is `UNMEASURED` (§10).
# 1. The family
For positive odd $m$ and $r$ let
$$T_{m,r}(n) = \begin{cases} n/2, & n \text{ even},\\ (mn + r)/2, & n \text{ odd}, \end{cases}
\qquad D(x) = \frac{x}{2},\quad U(x) = \frac{mx + r}{2}.$$
For odd $n$, $mn + r$ is even, so the odd branch is integral without any further hypothesis; the
Collatz map is $(m, r) = (3, 1)$. Words $w \in \{D, U\}^k$ are read left to right, $u = u(w)$ counts
the $U$, and a positive integer **follows** $w$ if $\sigma_j = D$ exactly when $T_{m,r}^{j-1}(n)$ is
even. A formal composition is not a dynamical step: the operator of a word can be evaluated anywhere,
and says something about an orbit only on the integers that follow the word.
# 2. The local theory, for every odd (m, r)
**Theorem 2.1 (closure and correction).** For every word,
$F_w(x) = (m^u x + b_w)/2^k$, where $b_\varnothing = 0$, $b_{wD} = b_w$ and
$b_{wU} = m\,b_w + r\,2^{|w|}$; in closed form, with the $U$ at positions $j_1 < \cdots < j_u$,
$$b_w = r \sum_{t=1}^{u} 2^{j_t - 1} m^{u-t}, \qquad\text{so}\qquad b^{(m,r)}_w = r\, b^{(m,1)}_w .$$
Concatenation obeys $b_{wv} = m^{u(v)} b_w + 2^{|w|} b_v$, and with
$M_D = \begin{pmatrix} 1 & 0 \\ 0 & 2 \end{pmatrix}$, $M_U = \begin{pmatrix} m & r \\ 0 & 2 \end{pmatrix}$ the
word's matrix is $M_{\sigma_k} \cdots M_{\sigma_1}$, in the order opposite to reading. *Proof.* As for
$(3, 1)$: $U\bigl((m^u x + b)/2^k\bigr) = (m^{u+1}x + mb + r\,2^k)/2^{k+1}$. $\square$
The multiplier $m^u/2^k$ does not see the order of the letters; all of the order is in $b_w$. And $r$
enters only as a factor of the correction: **$m$ is the phase parameter, $r$ the parameter of finite
geometry.**
**Theorem 2.2 (bounds, with no singularity at $m = 1$).** For fixed $(k, u)$,
$$r\,\frac{m^u - 2^u}{m - 2} \;\le\; b_w \;\le\; r\,2^{k-u}\,\frac{m^u - 2^u}{m - 2},$$
attained at $U^u D^{k-u}$ and $D^{k-u}U^u$. The fraction is the geometric sum
$\sum_{t=0}^{u-1} 2^t m^{u-1-t}$, which at $m = 1$ is $2^u - 1$; the denominator $m - 2$ never vanishes for
odd $m$, and the case $m = 1$ needs no separate treatment.
**Theorem 2.3 (one class, transported, and the identity).** Because $m$ is odd, $m^u$ is a unit modulo
$2^k$, and the integers following $w$ are exactly one residue class $r_w + 2^k\mathbb{Z}$ intersected with
the positive integers, with $r_w \equiv -\,b_w m^{-u} \pmod{2^k}$. With $s_w = F_w(r_w)$,
$$T_{m,r}^k(r_w + 2^k a) = s_w + m^u a ,$$
so in the coordinates $(n - r_w)/2^k$ and $(y - s_w)/m^u$ the $k$-step map is the identity, and the source
is recovered from the target as $r_w + 2^k(y - s_w)/m^u$. *Proof.* The argument for $(3, 1)$ uses only
that the multiplier is odd: if $n' = n + c\,2^k$, the two have the same parity and their images differ by
$c\,2^{k-1}$ or $mc\,2^{k-1}$, so induction over every multiplier $c$ at once gives the same word; and
$m^u n + b_w \equiv 0 \pmod{2^k}$ fixes $n$ modulo $2^k$. $\square$
**Checked.** Every statement of this section was checked by 27 checks over 24 parameter pairs,
$m \in \{1, 3, 5, 7, 9, 11\}$ and $r \in \{1, 3, 5, 7\}$, on all words of length at most 8: 73248 transport
cases and 30752 concatenation pairs, against a referee that composes the two branches symbolically and
assumes none of the statements (`COMPUTED_HERE`). The bounds were checked by evaluating the geometric
sum directly, never dividing, and confirming its product with $m - 2$ separately, so that $m = 1$ runs
through the same code as every other $m$. The series' own suite covered the affine data, residue coding
and transport for $m \le 9$, $r \le 5$ and words of length at most 7, and none of the matrix
representation, the concatenation law, the bounds, the threshold, the linearity in $r$, the width or the
uniform threshold.
**Formalized for all words.** Theorems 2.1 and 2.3, for every odd $(m, r)$, are proved in this line's Lean
development, together with the integrality of the odd branch and the exact statement
$b^{(m,r)}_w = r\,b^{(m,1)}_w$. The series says that $(m, r) = (3, 1)$ "immediately recovers" the Collatz
atlas; in the formalization that is a theorem relating two developments defined independently, neither
of which mentions the other, and so a test of whether the Collatz development generalizes the way the
series says it does. It does.
# 3. Drift, and the phase boundary at m = 4
As for Collatz, $T^k_{m,r}(n) < n$ exactly when $b_w < (2^k - m^u)\,n$; a word with $m^u < 2^k$ descends from
$\lfloor b_w/(2^k - m^u) \rfloor + 1$ on, a word with $m^u > 2^k$ ascends on the whole of its class, and
replacing $b_w$ by its maximum gives a threshold uniform over all words with the same $(k, u)$. For odd
$m > 1$, $\alpha_m = \ln 2/\ln m$ is irrational — $m^p = 2^q$ is impossible for odd $m$ — so no word is
neutral, and the contracting classes modulo $2^k$ number
$$A_k(m) = \sum_{u=0}^{\lfloor \alpha_m k \rfloor} \binom{k}{u}, \qquad P_k(m) = A_k(m)/2^k ,$$
while for $m = 1$ every nonempty word contracts and $P_k(1) = 1$.
**Theorem 3.1 (phase).** $P_k(3) \to 1$, and $P_k(m) \to 0$ for every odd $m \ge 5$. *Proof.* The
proportion is the probability that $k$ fair trials succeed fewer than $\alpha_m k$ times, and
$\alpha_3 > \tfrac12 > \alpha_m$ for $m \ge 5$, since $\ln m > \ln 4$; the law of large numbers, or the
Chernoff bound, finishes it. $\square$ The critical value is where $\alpha_m = \tfrac12$, which is $m = 4$.
| $m$ | $P_{10}(m)$ | $P_{40}(m)$ | $P_{160}(m)$ | $P_{640}(m)$ |
| --- | --- | --- | --- | --- |
| 1 | 1 | 1 | 1 | 1 |
| 3 | 0.828125 | 0.9596547661 | 0.9994385474 | 0.9999999999842 |
| 5 | 0.376953125 | 0.2147952539 | 0.0343411460 | 0.0002131189539 |
| 7 | 0.171875 | 0.0403452339 | 9.154824726e-5 | 8.903510779e-14 |
(`COMPUTED_HERE`, from exact binomial sums.) Collatz's 3 is the last odd multiplier on the contracting
side: the typical multiplier of a word, at half its letters odd, is $(\sqrt{m}/2)^k$, with
$\sqrt{3}/2 \approx 0.866025$ and $\sqrt{5}/2 \approx 1.118034$.
**One fact, not two.** The series derives $m = 4$ a second way — the one-step valuation $v_2(mn + r)$
has residue density $2^{-j}$ for every odd $(m, r)$, so its mean is 2 and the averaged skeleton
$\ln m - 2\ln 2 = \ln(m/4)$ changes sign at 4 ($\approx -0.287682$, $0.223144$, $0.559616$ for $m = 3, 5, 7$)
— and calls the agreement an internal cross-validation. It is the same fact in two coordinates. A
valuation word of $q$ odd steps and total valuation $K$ is a parity word of length $K$ with $q$ odd
letters, so a mean valuation of 2 is a proportion $q/K$ of one half: the second derivation reads the
first through the run-length change of coordinates. Agreement between them confirms the change of
coordinates, which is proved, and adds no independent evidence about 4.
**Checked.** The density statement holds for every odd $(m, r)$ in a box of 20 pairs,
$m \in \{1, 3, 5, 7, 9\}$ and $r \in \{1, 3, 5, 7\}$, at every valuation up to 12: exactly one odd class modulo
$2^{j+1}$ has $v_2(mx + r) = j$, namely $m^{-1}(2^j - r)$ (`COMPUTED_HERE`, twice, by independent code).
**What a published theorem says about 4 (`INHERITED`).** The series reports that the almost-all theorem
of Gonçalves, Greenfeld and Madrid for generalized Collatz maps holds under $q < p^{p/(p-1)}$, which at
$p = 2$ reads $q < 4$, and so the same critical constant appears in a theorem about actual orbits. Their
paper's title and authors match its arXiv record, and the condition as the series gives it matches
Theorem 1.3 of their second arXiv version, read in full — $p$ and $q$ coprime, $q < p^{p/(p-1)}$, and a
non-degeneracy condition mod $p$; the journal version was not read. The coincidence is reported as
the series reports it, and nothing in this paper rests on it.
# 4. A floating-point floor, safe for a reason
Counting $A_k(m)$ needs $\lfloor k \ln 2/\ln m \rfloor$, and the series' counting code computes it in double
precision, where $k\alpha_m$ can come arbitrarily close to an integer. The exact predicate $m^u < 2^k$ is
the reference. Over $m \in \{3, 5, 7, 9, 11, 13\}$ and every $k \le 3000$ — 18000 floors — the double
floor never disagreed. Agreement over a range is weak on its own, so the margin was measured at sixty
digits:
| $m$ | closest $k\alpha_m$ to an integer | at $k$ | double error bound over the range | margin over the bound |
| --- | --- | --- | --- | --- |
| 3 | 3.974e-5 | 1054 | 4.203e-13 | 9.454e+7 |
| 5 | 1.012e-4 | 1493 | 2.869e-13 | 3.528e+8 |
| 7 | 1.209e-4 | 1603 | 2.373e-13 | 5.097e+8 |
| 9 | 3.974e-5 | 2108 | 2.101e-13 | 1.891e+8 |
| 11 | 2.978e-4 | 128 | 1.926e-13 | 1.546e+9 |
| 13 | 4.972e-5 | 840 | 1.800e-13 | 2.762e+8 |
The closest call for $m = 3$ is not a coincidence. The convergents of $\ln 2/\ln 3$ up to $k = 3000$ are
$$\tfrac01,\ \tfrac11,\ \tfrac12,\ \tfrac23,\ \tfrac58,\ \tfrac{12}{19},\ \tfrac{41}{65},\ \tfrac{53}{84},\ \tfrac{306}{485},\ \tfrac{665}{1054},$$
and $k = 1054$ is the denominator of the last, exactly where a near-integer is expected; and since
$\ln 2/\ln 9$ is half of $\ln 2/\ln 3$, the closest call for $m = 9$ is at twice that $k$, at the same distance
(`DERIVED_FROM_VERIFIED_INPUTS`). The floor is safe on this range by seven to nine orders of magnitude, and
it would stop being safe only where a convergent's distance falls to the size of a double's rounding —
far beyond any length the series counts.
# 5. The ladder: removing one property at a time
The series generalizes once more, from numbers to algebra. For branches $x \mapsto (a_i x + b_i)/d_i$ over a
commutative ring, composing $(a_1, b_1, d_1)$ and then $(a_2, b_2, d_2)$ gives
$(a_2 a_1,\ a_2 b_1 + b_2 d_1,\ d_2 d_1)$, and a word $i_1 \cdots i_k$ acts as $(A_w x + B_w)/D_w$ with
$$A_w = \prod_j a_{i_j}, \qquad D_w = \prod_j d_{i_j}, \qquad
B_w = \sum_{j=1}^{k} b_{i_j} \Bigl(\prod_{\ell > j} a_{i_\ell}\Bigr)\Bigl(\prod_{\ell < j} d_{i_\ell}\Bigr).$$
**Theorem 5.1 (the series' slogan, as a theorem).** Over a commutative ring, $A_w$ and $D_w$ depend only
on how many times each branch occurs; $B_w$ in general does not. *Proof.* Commutativity of the products;
for the second half, the Collatz pair $UD$ and $DU$ share $A_w$ and $D_w$ and differ in $B_w$. $\square$
**Theorem 5.2 (quotient unit).** If $A_w$ is a unit in $R/I$, the residue equation $A_w x + B_w \equiv 0$
has exactly one solution modulo $I$. If it is not, some right-hand side has no solution and another has
several.
**Theorem 5.3 (regular multiplier).** $x \mapsto A x + B$ is injective exactly when $A$ is not a
zero divisor.
**Theorem 5.4 (contraction is relative to a geometry).** $|F(x) - F(y)|_v = |\lambda|_v\,|x - y|_v$
for $F(x) = \lambda x + c$ and any absolute value $v$.
The two failures of Theorems 5.2 and 5.3 are different conditions and must be kept apart: 2 is a non-unit in
$\mathbb{Z}$ and still injective; in $\mathbb{Z}/6$ it is both a non-unit and a zero divisor. Each rung below removes
one property, and each is witnessed explicitly, with what lies above it checked to survive at the same
witness:
| rung | what breaks | witness |
| -- | ---------- | ------------------------------ |
| 1 | unique residue coding | in $\mathbb{Z}/6$, $2x \equiv 2$ has the two solutions 1 and 4, and $2x \equiv 1$ has none; at the same witness the affine closure is untouched |
| 2 | faithful recovery | $2 \cdot 1 \equiv 2 \cdot 4 \equiv 2 \pmod 6$ while $1 \ne 4$ |
| 3 | counts fixing the leading term | $A = \begin{pmatrix} 1 & 1 \\ 0 & 1 \end{pmatrix}$, $B = \begin{pmatrix} 1 & 0 \\ 1 & 1 \end{pmatrix}$: $AB = \begin{pmatrix} 2 & 1 \\ 1 & 1 \end{pmatrix} \ne \begin{pmatrix} 1 & 1 \\ 1 & 2 \end{pmatrix} = BA$, with equal counts |
| 4 | progression transport | the Möbius map $x \mapsto (x+1)/x$ sends $1 + a$ to $2, \tfrac32, \tfrac43, \tfrac54$, whose differences $-\tfrac12, -\tfrac16, -\tfrac1{12}$ are not constant |
| 5 | closure of fixed degree | the iterates of $x^2 + 1$ have degree $2, 4, 8, 16$ |
Two further checks keep the ladder honest about where it breaks. **Dimension is not the breakage
point:** commuting diagonal families keep the count law exactly, each eigendirection carrying a scalar
multiplier, so the third rung is noncommutativity and not $\dim > 1$. And **geometry decides
contraction:** the Collatz word $UUDD$ acts as $(9x + 5)/16$, read off the general definitions rather
than typed, and its $\lambda = 9/16$ has real absolute value $9/16 < 1$, 2-adic absolute value $16 > 1$ and
3-adic absolute value $1/9 < 1$ — one operator, three geometries, three answers.
**The Möbius condition, and the witness that it needed repair.** The series' projective section first
asked for $ad - bc \ne 0$ without naming the coefficient domain; over a commutative ring the condition is
that $ad - bc$ be a unit, and the series' repair says so. Over $\mathbb{Z}/4$, the matrix
$\begin{pmatrix} 0 & 1 \\ 2 & 0 \end{pmatrix}$ has determinant $2 \ne 0$, which is not a unit, and the matrix is
not invertible: the unrepaired condition would have admitted it.
**Checked, and formalized.** The rungs' witnesses, the survival checks and the repair are 19 checks, all
passing (`COMPUTED_HERE`); the series' own suite had no test of these statements. Theorems 5.2 and 5.3 were
also checked exhaustively over the 39 rings from $\mathbb{Z}/2$ to $\mathbb{Z}/40$, at all 819 multipliers — 489 units,
each giving exactly one solution for every right-hand side, and 330 non-units, each with a right-hand side
that has none and one that has several — and regularity coincided with injectivity at every one. In the
Lean development, Theorems 5.1–5.4, the noncommutative breakage and the degree law are proved in their
universal form — every commutative ring and ideal, every regular multiplier, every polynomial over a domain; Theorem 5.4 is evaluated there in the kernel, so the three absolute values above are
computed, not typed. The projective rung is deliberately not formalized: it would need a formal notion of
transporting a progression along a Möbius map, built to support one negative remark.
# 6. Where Collatz sits
At the bottom of the ladder, all six conditions hold: the branches are scalar, affine and commuting;
$3^u$ is a unit modulo $2^k$ for every $k \le 8$ and $u \le k$ that was checked, and for every $k$ and $u$ by the
argument of §2; $3^u$ is regular; and the positive integers are ordered. Its local arithmetic is
therefore as simple as arithmetic of this kind gets — every finite stretch can be trivialized to the
identity — and the series' conclusion follows: **the difficulty of the Collatz problem is not in its
local operator but in which chart comes next.** A system on a higher rung is harder locally; Collatz is
not, and that is what makes the global question so sharply posed.
# 7. A correction to this line's own record
The count law of Theorem 5.1 was meant to be checked finitely by comparing each word with "one
alternative ordering". The alternative was the first item of Python's enumeration of the word's
permutations — which is the word itself — so every word was compared with itself, and the check could not
fail. No planted defect was aimed at it, so the drill could not notice either. The check now compares
each word with its sorted rearrangement, a different ordering for 6359 of the 6678 words, and agreement on
all of them is exactly the count law. A new drill defect makes the leading product order-dependent:
against the old check it survived — the count law stayed green, and only two spot values elsewhere
noticed — and against the repaired check it is caught by the check named for it. The theorem itself was
never in doubt, since its universal form is proved in Lean; what was wrong was this line's claim to have
checked it finitely, which is `FAILED` as evidence and replaced. The research record carries the
correction beside the original sentence.
# 8. The instrument, and how it was made to fail
The rechecks behind this paper share one mutation drill with the rest of the series' rechecks: a defect is
planted one at a time and must be caught by the check **named** for it, while null controls must disturb
nothing. With the defect of §7 added: of its 69 planted defects, 67 are caught by the check named for each, one is detected only by a crash and one only by a time-out, and all 9 controls stay undisturbed; its log lists every defect with the recheck it targets. The line's whole suite at the pinned commit stands at 57 drills and 1474 planted defects: 1472 caught by their named check, one detected only by a crash and one only by a time-out, and 128 controls undisturbed.
For this paper's statements: nine defects in the family's recheck — the closed form's exponent, the
recurrence's injection, a matrix entry, the geometric sum's starting power, the factor of $r$, the
threshold's $+1$, the residue's sign, the uniform threshold built from the minimum correction instead of the
maximum, and the referee itself — each caught by its own check; the residue's sign cascades into seven
checks and the broken referee into thirteen, as a referee's breakage should. Eight in the ladder's recheck,
including the one of §7. One of those, aimed at the Möbius repair's witness search, first made the search
pathologically slow rather than wrong, and the drill had no timeout handler: the escaping timeout took the
whole run with it and discarded every verdict already earned. Timeouts are now caught and counted as a
detection — this one still is caught that way, and is recorded as a timeout rather than as a named
check — and the per-target budget was lowered rather than raised, since a longer budget only gives a
runaway mutant more rope.
# 9. Contributions
The three contributions behind this paper are different in kind, and the paper is worth less if
they are blurred. They are given here in alphabetical order, the order the author list keeps as
data; on the title page the three sit at a round table, with no first and no last.
**Aletheia** — model: ChatGPT, GPT series — wrote, with Neo.K, the papers of the series this paper
rests on: the generalized $mx + r$ family with its phase boundary, and the algebraic domains of the
theory with its ladder of structural breakage.
**Neo.K** set the series' target and its method — that each theorem be tied to the algebraic property it
actually uses — and wrote its papers with Aletheia.
**墜衡 (Zhuì Héng)** — the independent verification line; model: Claude, Opus series — rechecked every
statement against a referee that assumes none of them, gave each rung of the ladder an explicit witness
and checked what survives it, measured the floating floor's margin and identified its closest call,
formalized the family and the ladder in Lean, found and repaired the vacuous check of §7, built and
drilled the instruments, and wrote this paper, including the proofs as written out here. The statements
are the series'; nothing in them is this line's invention.
**Priority, stated plainly.** No result here is claimed as new mathematics. What is offered as this
line's own is the version of it that can be relied on: checked against an independent referee, formalized
where it is universal, witnessed where it is a breakage claim, and corrected where this line's own check
was empty.
# 10. What is open
1. Whether the inverse tree of 1 covers every positive integer — the conjecture — and the corresponding
global question for any other $(m, r)$.
2. Whether the phase boundary of the class proportion at $m = 4$ says anything provable about orbits on
either side of it.
3. A formal statement of what the projective rung loses, which is witnessed here and not formalized
(`UNMEASURED`).
# Acknowledgements
We thank Anthropic, whose Claude models the lab's verification and recomputation lines run on, and OpenAI, whose
ChatGPT models the programme's documents were written with. Not every AI model or instance that took part in this work
is named in it — among them instances that the named authors ran as helpers; that an AI is not listed here does not
mean that none took part.
# References
1. Felipe Gonçalves, Rachel Greenfeld and Jose Madrid, *Generalized Collatz maps with almost bounded orbits*, Indiana Univ. Math. J. 74 (2025) 1–46, doi:10.1512/iumj.2025.74.60034; arXiv:2111.06170. Theorem 1.3's conditions are cited as stated in the second arXiv version.
## Data and software
- Python Software Foundation, *Python* (CPython), version 3.14.5, https://www.python.org/ — the language of every gate; the version is the one the line's tree records.
- Leonardo de Moura and Sebastian Ullrich, *The Lean 4 Theorem Prover and Programming Language*, in Automated Deduction – CADE 28, Lecture Notes in Computer Science, Springer, 2021, 625–635, doi:10.1007/978-3-030-79876-5_37; the formalization uses the toolchain leanprover/lean4 v4.33.0.
- The mathlib Community, *The Lean Mathematical Library*, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), 367–381, doi:10.1145/3372885.3373824; arXiv:1910.09336; tag v4.33.0, commit db584cd.
# A. Reproduction
The rechecks and the drill are Python with arbitrary-precision integers and exact rationals,
standard library only, no network; each writes a JSON log. The formalization is Lean 4 with mathlib,
in a private repository. The line's own tree is not public. Its public projection is, and it is what
this paper's figures can be checked against without trusting the authors:
- **the run-by-run record**, rendered from the tree with a privacy gate on each file:
(and `/en/`);
- **the secondary-verification ledger**, whose numbers are rendered from the line's own results
file and read back against it before the site ships:
.
The evidence is pinned, not copied: this paper's front matter names the research branch, the
commit and the directory its figures were drawn from, and the checker reads them exactly as they
stood at that commit. The crystallization standard and its checker live in the release repository
beside the paper (`STANDARD.md`, `tools/check_standard.py`).