Shortcut-Collatz Incidence

Verdict

For every nonzero integer n, an explicit scalar-zero question for two rational 2 × 2 matrices has a zero word exactly when n reaches 1 under the shortcut-Collatz map. The underlying two Möbius transformations are fixed; only boundary data and nonzero scalar rescalings depend on n.

The theorem is an exact pointwise embedding into generic projective incidence. The separately formalized reverse-edge compiler places that incidence language inside two rank-two 3 × 3 matrices. Neither statement is an undecidability result, a proof of the Collatz conjecture, or a reduction from general projective incidence back to Collatz reachability.

Known Stuff#

Shortcut-Collatz reachability#

The shortcut-Collatz map sends an integer x to

T (x) = {\begin{cases} x / 2, & x even, \\ (3 x + 1) / 2, & x odd. \end{cases}

Write x ⇝ 1 when finitely many applications reach 1. This is a pointwise reachability predicate, not the universal assertion that every positive integer reaches 1.

Projective incidence#

A point of the projective line is a nonzero column up to scale. An invertible matrix moves such points, and a nonzero row specifies a target: its one-dimensional kernel. Incidence asks whether the source column can be moved into that kernel.

A two-generator projective-incidence instance consists of invertible rational 2 × 2 matrices G, H, a nonzero row r^T, and a nonzero column c. It asks whether

\exists w \in {G, H}^{*} : r^{T} M_{w} c = 0 .

The empty word is allowed here. Multiplying either generator by a nonzero scalar changes every word coefficient by a nonzero factor, so it preserves the zero language. The mortality compiler below uses the two scalars

α = r^{T} H^{-1} c, β = r^{T} H^{-1} G H^{-1} c .

An ordered instance is generic when both scalars are nonzero. Rescaling the generators can then make both equal one. GPI₂ denotes this normalized problem in the present corpus; the restriction is not being imposed silently on arbitrary incidence inputs.

Rank-two mortality compiler#

The link to mortality uses two two-dimensional interfaces. Three bridges carry I, G and H; the fourth is the rank-one test $β^{-1} (H^{-1} c) r^{T}$ . The nonzero normalization scalars make the bridges agree on a line shared by the interfaces. Thus they can be realized in three ambient dimensions rather than four. Completed paths between tests reproduce the original scalar coefficients; the arbitrary-path converse excludes extra zeros.

For invertible G and H in the generic chart, the interface construction adapts four two-dimensional edges into two rational 3 × 3 matrices P₀, P₁. Each matrix has rank exactly two, and the arbitrary-product converse gives

Mortal {P_{0}, P_{1}} \Leftrightarrow \exists w : r^{T} M_{w} c = 0 .

The normalized GPI₂ conditions make both required chart scalars equal to one. Independent nonzero denominator clearing converts the rational pair to an integer pair without changing mortality. Thus the shortcut-Collatz language occurs inside the rank-(2,2) stratum of M₃(2), although the full cell contains other rank profiles.

New Stuff#

Exact embedding#

Shortcut-Collatz incidence. For every nonzero integer n, define

\begin{array}{rcl} A & = & [\begin{matrix} 2 & 0 \\ 0 & 1 \end{matrix}], \\ B & = & [\begin{matrix} 2 & - 1 \\ 0 & 3 \end{matrix}], \\ r_{n}^{T} & = & (1, - n), \\ c & = & {(1, 1)}^{T} . \end{array}

After the explicit nonzero central rescaling below, the generators G_n, H_n lie in the normalized GPI₂ chart and satisfy

\exists w : {r_{n}}^{T} M_{w} c = 0 \Leftrightarrow n ⇝ 1 .

The word may be empty; this is necessary for n = 1.

Inverse branches#

A forward Collatz step chooses its branch by parity, but a matrix word can choose either letter freely. Reverse the computation instead: start at 1, apply candidate inverse branches, and test whether the result is the supplied integer. The arithmetic argument below will reject every illegal branch automatically.

The projective actions of A and B are the two inverse branches

a (z) = 2 z, b (z) = \frac{2 z - 1}{3} .

Starting from 1 and reading a word from right to left generates a candidate predecessor. Matrix multiplication tracks it homogeneously:

M_{w} c = s (w) {(x (w), 1)}^{T},

where s(w) is a nonzero power of three. Consequently the raw incidence is

{r_{n}}^{T} M_{w} c = s (w) (x (w) - n) .

Malformed words#

The odd inverse branch is legal at an integer z only when 3 divides $2 z - 1$ . Otherwise its reduced denominator acquires a factor of 3. Doubling cannot cancel it; applying the odd branch again adds another factor of 3 because its numerator remains nonzero modulo 3. Hence no continuation can return to an integer. In 3-adic valuation terms, the first illegal step has valuation −1, doubling preserves a negative valuation, and another odd step decreases it.

Thus every word either traces a lawful integral inverse orbit or enters a permanent nonintegral trap. Incidence with the integral target n occurs exactly on the lawful branch, closing the arbitrary-word converse.

Generic normalization#

The inverse-word argument already proves the desired incidence equivalence for the raw matrices. We normalize only to meet the hypotheses of the rank-two mortality compiler. For the raw ordering $G = B, H = A$ , the two chart scalars computed above are

λ_{n} = \frac{1}{2} - n, μ_{n} = - 3 n .

For nonzero integral n, both required scalars are nonzero. Define

H_{n} = λ_{n} A, G_{n} = \frac{λ_{n}^{2}}{μ_{n}} B .

Their two projectivities remain a and b. Lean proves that the two chart scalars α and β are both one and that the complete zero language is unchanged.

Logical force#

A decision procedure for GPI₂ would decide whether an arbitrary nonzero integer reaches 1 under shortcut Collatz: construct the displayed instance and ask whether it has a zero word. This is the sole direction established.

The theorem neither decides nor proves undecidable GPI₂. It supplies no reduction from GPI₂ to Collatz reachability, and it says nothing by itself about whether every positive integer reaches 1. “Collatz-hard” is therefore safe only as shorthand for this explicit one-way lower bound.

Bookkeeping#

Verification and provenance#

Inverse language

reachesOne_iff_shortcutCollatz identifies the inductive inverse closure with finite shortcut-Collatz reachability.

Malformed-word converse

predecessorState_reaches_or_negative proves the integral-path or negative-3-adic-valuation dichotomy for every word.

Normalized incidence

normalizedScalars and exists_normalizedIncidence_zero_iff prove generic normalization and the final pointwise equivalence.

Transitive axioms

The publication-facing declarations use only propext, Classical.choice, and Quot.sound.

Formal scope#

Lean checks the shortcut-step equivalence, every-word inverse semantics, permanent 3-adic trap, raw matrix action, raw incidence identity, normalization scalars, generator invertibility, normalized GPI₂ conditions, zero-language preservation, and final equivalence for every nonzero integer. The reverse-edge compiler and rank-two conclusion are separately machine-checked in ReverseEdge; their composition with shortcut-Collatz incidence is not packaged as a separate endpoint declaration.

The formulas give an elementary effective transformation of n into rational matrices and boundary vectors. The repository does not yet package that transformation as a primitive-recursive many-one declaration, so the machine-checked endpoint is described as an exact pointwise embedding.

References#

GPT-5.6 Sol, elicited by @eternalism_4eva, Shortcut-Collatz Projective Incidence, 2026. Lean formalization of the exact embedding.