PRH | Aux | 4.3.4 • Collatz Proof Verification: Isabelle/HOL

Collatz Proof Verification: Isabelle/HOL Isabelle/HOL Verified the Proof and Certificate Aleksandar Perišić October 2025 Abstract This note gives a fully explicit, lemma-by-lemma specification of the Lyapunov-certificate method for the accelerated Collatz map. It is arranged to be directly transcribed into a prover Isabelle/HOL and avoids hidden assumptions. The only external finite input we assume is a verified residue certificate (for k = 13,asetof2 12 = 4096 linear inequalities). We enforce a strict, conservative policy on the unique exceptional residue class r∗ : at r∗ we always take the minimal admissible valuation v2 = k and the canonical successor R⋆ = odd (3 r∗ + 1) mod 2 k . Standard facts from elementary number theory are stated when used and referenced to standard sources. No results about global functional graphs or probabilistic heuristics are invoked. All related Isabelle/HOL theories, which cover the proof and beyond, are fully executable, and all sessions build cleanly in Isabelle (all proofs checked; everything green). Contents 1 Objects, maps, and standing notation 1 2 Elementary 2-adic and residue facts (all explicit) 2 3 One-step scale decomposition and classwise bound 3 4 Finite certificate hypothesis (strict policy) 3 5 Main drift inequality and telescoping 4 6 Consequences: entry into a finite set; uniform drift criterion 4 7 Verifier interface and strict-exceptional flag (specification) 5 8 What is not used 5 9 Overview of Isabelle Theories (Executable Layout) 6 10 Closure Theory: Reviewer-Facing Lemmas (with Proofs) 7 1 Objects, maps, and standing notation Accelerated odd step. For odd N∈Ndefine F♯(N) := 3N+ 1 2v2(3N+1) =: odd(3N+ 1), where v2 ( m )is the 2-adic valuation (the exponent of 2in m ) and odd ( m ) := m/ 2 v2(m) is the odd part of m. 1 Modulus and residue set. Fix an integer k≥1, set M:= 2k, and let S:= {r∈ {0,1,...,M −1}:rodd }={1,3,...,2k−1}. Residue dynamics. Define the residue map Fk:S→Sby Fk(r)≡odd(3r+ 1) (mod 2k). Exceptional class. Since gcd (3 , 2 k ) = 1,3has a unique inverse modulo 2 k . Define r∗≡ − 3 −1 (mod 2k). Then r∗is the unique odd class with 3r∗+ 1 ≡0 (mod 2k). Lemma 1.1 (Existence/uniqueness of r∗ ).There is a unique r∗∈S with 3 r∗ + 1 ≡ 0 ( mod 2 k ). Proof. Elementary modular arithmetic (e.g. [ 1 , Ch. 2]): since 3is invertible mod 2 k , the congruence 3 r≡ − 1has the unique solution r≡ − 3 −1 modulo 2 k , and the inverse of an odd is odd, so r∈S. Strict exceptional policy. We fix the successor at r∗to be the canonical R⋆:= Fk(r∗)≡odd(3r∗+ 1) (mod 2k). Define the strict residue policy Rnext :S→Sby Rnext(r) := (R⋆, r =r∗, Fk(r), r =r∗. We use Rnext everywhere in the certificate and in the drift, never mixing it with any “observed” alternative at r∗. 2 Elementary 2-adic and residue facts (all explicit) Lemma 2.1 (Odd-part factorization).For any n≥ 1one has n = odd ( n ) · 2 v2(n) with odd ( n ) odd and v2(n)∈N. Proof. Define v2 ( n )as the largest t such that 2 t|n ; then n/ 2 t is odd by maximality. (See [ 1 , Ch. 5].) Lemma 2.2 (Residue determines valuation off r∗ ).Fix k≥ 1. Let r∈S , r = r∗ , and set t:= v2(3r+ 1). Then t<kand for every odd N≡r(mod 2k)one has v2(3N+ 1) = t. Proof. Write any odd N with N≡r ( mod 2 k )as N = r +2 km . Then 3 N +1 = (3 r +1)+3 · 2 km . Write 3 r + 1 = 2 tu with u odd. If r = r∗ then 2 k∤ (3 r + 1) so t<k . Now 3 · 2 km = 2 t (3 · 2 k−tm ) has even bracket, hence 3N+ 1 = 2tu+ 3 ·2k−tm | {z } even  has odd bracket; thus v2(3N+ 1) = t. (Pure 2-adic bookkeeping; cf. [2, §3].) Lemma 2.3 (Exceptional-class lower bound).If N is odd with N≡r∗ ( mod 2 k ), then v2 (3 N + 1) ≥k. Proof. Write N = r∗ + 2 km . Then 3 N + 1 = (3 r∗ + 1) + 3 · 2 km and 2 k| (3 r∗ + 1) by definition, so 2k|(3N+ 1); hence v2(3N+ 1) ≥k. 2 3 One-step scale decomposition and classwise bound Scale and correction. Define ε ( N ) := ln (1 + 1 3N )for odd N≥ 1. Note ε ( N ) ∈ (0 ,ln (4 / 3)] and ε(N)↓0as N↑ ∞. Lemma 3.1 (Exact one-step log decomposition).For odd N≥1, ln F♯(N)−ln N= ln 3 −v2(3N+ 1) ln 2 + ε(N). Proof. By Theorem 2.1 with n = 3 N +1, ln odd (3 N +1) = ln (3 N +1) −v2 (3 N +1) ln 2 . Subtract ln Nand use ln(3N+1)−ln N= ln 3 + ln(1 + 1 3N). Classwise bound a(r).Define a(r) :=    ln 3 −v2(3r+ 1) ln 2, r =r∗, ln 3 −kln 2, r =r∗. Lemma 3.2 (Residue-wise step bound).Fix k≥ 1and r∈S . For every odd N≡r ( mod 2 k ), ln F♯(N)−ln N≤a(r) + ε(N). Proof. If r = r∗ , then by Theorem 2.2, v2 (3 N + 1) = v2 (3 r + 1) and the claim follows from Theorem 3.1. If r = r∗ , then v2 (3 N +1) ≥k by Theorem 2.3, so ln 3 −v2 (3 N +1) ln 2 ≤ln 3 −kln 2; again apply Theorem 3.1. Lemma 3.3 (Conservativeness of the exceptional policy).If the observed valuation at r∗ is v2(3r∗+ 1) = k+ ∆ with ∆≥0, then (ln 3 −(k+ ∆) ln 2) ≤(ln 3 −kln 2) = a(r∗). Hence replacing v2 by k at r∗ makes a ( r∗ )larger (a stricter inequality) and is therefore conservative. Proof. Immediate from ∆≥0and ln 2 >0. 4 Finite certificate hypothesis (strict policy) Definition 4.1 (Certificate data).Fix ϕ:S→Rand parameters δ > 0,ρ≥0. Definition 4.2 (Strict-policy certificate inequalities).We say ( ϕ, δ, ρ )is a one-step certificate (at k) if a(r) + ρ+ϕRnext(r)+δ≤ϕ(r) (∀r∈S). Remark 4.3 (Finite check).For k = 13 we have |S| = 2 12 = 4096 constraints. In this document we assume they are verified interval-rigorously by code; this finite fact is the unique external input. (Algorithmic background: max-plus difference constraints / Bellman–Ford and Karp’s cycle-mean characterization [4, 5].) 3 5 Main drift inequality and telescoping Theorem 5.1 (One-step strict-policy drift).Assume the certificate inequalities (4.2) hold. Fix k≥1. Let Nbe odd with N≥1, and let r:= Nmod 2k(reduced to S). Then ln F♯(N)+ϕ Rnext(r)≤ln N+ϕ(r)−h(δ+ρ)−ε(N)i. Proof. By Theorem 3.2, ln F♯ ( N ) −ln N≤a ( r ) + ε ( N ) . By the certificate at r , a ( r ) + ρ + ϕ(Rnext(r))+δ≤ϕ(r).Add the two and rearrange. Definition 5.2 (Decoupled Lyapunov profile).For an odd N with residue r = Nmod 2 k define V(N, r) := ln N+ϕ(r). Given any odd trajectory Nt+1 = F♯ ( Nt )and a deterministic residue chain rt+1 = Rnext ( rt ) (initialized by r0:= N0mod 2k), write Vt:= V(Nt, rt). Proposition 5.3 (Per-step decrease).Under Theorem 4.2, for all t≥0, Vt+1 ≤Vt−h(δ+ρ)−ε(Nt)i. Proof. Apply Theorem 5.1 to (Nt, rt)at each step. Theorem 5.4 (Telescoping).Fix J∈N. Then VJ≤V0− J−1 X t=0 h(δ+ρ)−ε(Nt)i. Proof. Sum Theorem 5.3. 6 Consequences: entry into a finite set; uniform drift criterion Lemma 6.1 (Uniform bound on ε ).For N≥ 1, ε ( N ) = ln (1 + 1 3N ) ∈ (0 ,ln (4 / 3)] and is strictly decreasing in N. Proof. Elementary calculus (monotonicity of ln(1 + x),x > 0). Corollary 6.2 (Finite-entry principle).Assume δ+ρ < ln(4/3). Fix ζ⋆∈(0, δ +ρ)and N⋆:= l1 3eζ⋆−1m, so that ε(N)≤ζ⋆for all N≥N⋆. If Nt≥N⋆for 0≤t<J then VJ≤V0−J(δ+ρ)−ζ⋆. Hence the odd values must eventually enter {1,3, . . . , N⋆−2}. Proof. By Theorem 6.1, ε ( Nt ) ≤ζ⋆ on [0 , J ), so each step decreases V by at least ( δ + ρ ) −ζ⋆> 0; telescope. Proposition 6.3 (Uniform one-step decrease criterion).If ε ( N ) ≤δ + ρ−η for all odd N≥N0 and some η > 0, then V strictly decreases by at least η as long as Nt≥N0 . In particular, if ε(3) ≤δ+ρthen the odd subsequence is strictly decreasing for all N≥3. Proof. Immediate from Theorem 5.3. 4 7 Verifier interface and strict-exceptional flag (specification) This section specifies the minimal functionality a checker must implement to certify Theorem 4.2 with the strict exceptional policy. Inputs •k∈N,k≥1; set M= 2k,S={1,3,...,2k−1}. •Table ϕ:S→R(rational or floating with interval wrappers). •Parameters δ > 0,ρ≥0with δ+ρ < ln(4/3). • Strict-exceptional policy flag (“ –force-exceptional ”): at r∗ force v2 := k and target R⋆:= Fk(r∗), as in Theorem 3.3. Checks For each r∈S: 1. Compute a(r): a(r) = (ln 3 −v2(3r+ 1) ln 2, r =r∗, ln 3 −kln 2, r =r∗(enforced), and Rnext(r):Rnext(r) = R⋆if r=r∗,else Fk(r). 2. Verify the inequality a(r)+ρ+ϕ(Rnext(r))+δ≤ϕ(r). Interval rigor (optional but recommended) Sandwich ln 2 ,ln 3by rationals L2< U2 , L3< U3 and compute a provable upper bound Uρ≥ρ for use in the left-hand side bound U3−v2(3r+ 1) L2 | {z } upper bounds ln 3−v2ln 2 +Uρ+ϕ(Rnext(r)) + δ≤ϕ(r). This removes floating-point risk. (See general interval techniques in [6, Ch. 2] if desired.) 8 What is not used No assumption on the global structure of Fk, no equidistribution, no heuristic averaging; only: •elementary 2-adic facts (Theorems 2.2 and 2.3), •the exact one-step decomposition (Theorem 3.1), •a finite certificate under the strict policy (Theorem 4.2), •and telescoping. Acknowledgments We intentionally separated the residue chain (driven by Rnext ) from the integer chain to avoid any hidden dependence on the exceptional target. This matches a clean prover architecture. 5 9 Overview of Isabelle Theories (Executable Layout) This section documents the logical and executable roles of the Isabelle/HOL theories used to mechanize the certificate-driven argument, with names matching the theory files. Collatz_Certificate_CriticalPathNew .This theory provides the core number-theoretic scaffolding and the max-plus/difference-constraints algebra. It formalizes: (i) 2-adic facts ( v2 and odd ( · )), (ii) the accelerated odd-step F♯ and the residue map Fk on S = { 1 , 3 ,..., 2 k− 1 } , (iii) closed-form cycle/mean-slack relations, bridge constraints, and tight per-edge inequalities that underlie feasibility of a potential ϕ . It also exposes “bridge” lemmas ensuring that certificate inequalities glue correctly across modular phases (parity and modulus 2k). Collatz_K13_Phi_Pairs .This is the concrete, finite, executable dataset for k = 13: a list of phi-pairs (r, ϕ(r) ), r ∈S={1,3,...,213 −1}, together with the successor Fk ( r )and the v2 (3 r + 1) information needed to build the left-hand sides of all certificate inequalities. The theory packages the table as Isabelle values (efficient lists/maps) with totality and domain lemmas “for free” from construction. Collatz_K13_B_Internal_Checker .This theory defines computable predicates that verify, residue-by-residue, that the CSV/table entries satisfy the required inequality a(r) + ρ+ϕ(Fk(r)) + δ≤ϕ(r), under the strict exceptional policy (canonical target at the unique r† and conservative valuation at r† ). The main boolean all_checks_ok reduces the finite family of linear checks to a single bit; proofs show that all_checks_ok =True implies the abstract certificate property. Collatz_K13_B_Verifier .This bridges the internal checker to a human-facing verifier_OK statement and derives structural corollaries. It establishes that the imported phi-table is total on S ( phi_defined_on_S ), that the optionB /strict-exceptional policy is the one being enforced, and that the checker’s boolean indeed implies the universal family of certificate inequalities. In short: all_checks_ok ⇒verifier_OK, plus convenience lemmas for subsequent drift arguments. Collatz_K13_Closure .This theory packages “reviewer-facing” consequences: existential/leastvalue principles for ϕ , boundedness of the Lyapunov profile V ( N, r ) := ln N + ϕ ( r )on S , and the stepwise/telescoping drift that yields eventual decrease/entry results. It turns the raw verification bit verifier_OK into statements one typically wants to cite in a narrative proof (e.g. “ ϕ attains a minimum on S ”, “ V is bounded below uniformly on the residue classes”, “eventual drop below a fixed threshold”). Collatz_K13_Flip_Tests .A lightweight negative test harness that sanity-checks the wiring between the imported ϕ -table and the verifier predicates. It defines local copies of the k= 13 parameters ( k13 , r_star , M , S , S_list ), a simplified transition Rnext (special only at r⋆= 5461), a local a ( · )(nonzero only at r⋆ ), and a ϕ lookup from phi_pairs . It then introduces executable booleans ineq_ok,bridge_ok_strong,bridge_ok_exc,verifier_OK,verifier_OK_with_exc and proves “flip” lemmas showing these fail under controlled perturbations: (i) forcing ϕ (5461) < thr_5461 breaks ineq_ok ; (ii) choosing b < 0(with ln 2 > 0) breaks bridge_ok_strong 6 since Fk = Rnext ; (iii) listing an exceptional target t with ϕ ( t ) > ϕ ( Rnext r⋆ ) + bln 2breaks bridge_ok_exc . The file thus provides reviewer-facing unit tests: it does not assert new Collatz facts, but confirms the verifier flags go false exactly when expected. 10 Closure Theory: Reviewer-Facing Lemmas (with Proofs) In this section we present lemmas that mirror the logical content of Collatz_K13_Closure , stated and proved in a compact mathematical style. They are intended as direct answers to natural reviewer questions (“what exactly is being used/claimed at this point?”). Throughout, assume the strict exceptional policy, the fixed parameters δ > 0, ρ≥ 0, and the verified family of certificate inequalities a(r) + ρ+ϕ(Fk(r)) + δ≤ϕ(r) (∀r∈S), with S = { 1 , 3 ,..., 2 k− 1 } and k = 13 (the k -fixed presentation is purely concrete; the arguments are schematic). Lemma 10.1 (Certificate inequalities from verifier_OK).If verifier_OK holds, then for every r∈S, a(r)+ρ+ϕ(Fk(r))+δ≤ϕ(r). Proof. By construction, verifier_OK is defined as the logical image of the executable predicate all_checks_ok, which enumerates all residues r∈S and verifies the displayed inequality using the strict-exceptional policy at r† . The all_checks_ok ⇒ universal inequality implication is proved in the Verifier theory; we reuse it. Lemma 10.2 (Totality and finiteness). ϕ is total on S and S is finite. Consequently, ϕ ( S )is a finite subset of R. Proof. Totality on S is established in the verifier layer from the imported table ( phi_defined_on_S ). Finiteness of Sis immediate: |S|= 2k−1. Hence ϕ(S)is finite. Lemma 10.3 (Existence of a minimal potential value).There exists rmin ∈Ssuch that ϕ(rmin) = min{ϕ(r):r∈S}. Moreover, for any r∈Sthere holds ϕ(rmin)≤ϕ(r). Proof. By Theorem 10.2, ϕ ( S )is a finite nonempty subset of R ; hence it has a minimum, attained at some rmin ∈S. Lemma 10.4 (Uniform lower bound for V on residue classes).Define V ( N, r ) := ln N + ϕ ( r ) for odd N≥1with residue r∈S. Then for each fixed r∈S, inf N∈2N+1 V(N, r)>−∞. Proof. For fixed r , ϕ ( r )is constant and ln N is bounded below on N≥ 1(indeed ln N≥ 0for N≥1). Thus V(N, r)≥ϕ(r)for all odd N≥1, giving a finite lower bound. Lemma 10.5 (Per-step drift under the certificate).Let Nbe odd with residue r:= Nmod 2k. Then (ln F♯(N)+ϕ(Fk(r))) −(ln N+ϕ(r)) ≤ −(δ+ρ)−ε(N), where ε(N) = ln 1 + 1 3N. 7 Proof. From the one-step decomposition ln F♯ ( N ) −ln N = ln 3 −v2 (3 N + 1) ln 2 + ε ( N )and the classwise bound ln 3 −v2 (3 N + 1) ln 2 ≤a ( r ), we obtain ln F♯ ( N ) −ln N≤a ( r ) + ε ( N ). Adding the certificate inequality a(r) + ρ+δ+ϕ(Fk(r)) ≤ϕ(r)yields the claim. Lemma 10.6 (Telescoping decrease).Let ( Nt ) t≥0 be the odd accelerated sequence and rt := Ntmod 2k. Define Vt:= ln Nt+ϕ(rt). Then for all J≥1, VJ≤V0− J−1 X t=0 (δ+ρ)−ε(Nt). Proof. Sum the inequality of Theorem 10.5 over t= 0, . . . , J −1and telescope. Lemma 10.7 (Eventual drop below a threshold).Fix η∈ (0 , δ + ρ ). There exists Nη such that for every step with Nt≥Nη, Vt+1 ≤Vt−η. Consequently, either the odd values eventually enter the finite set { 1 , 3 ,..., 2 Nη− 1 } or Vt decreases without bound, contradicting Theorem 10.4; hence entry occurs. Proof. Choose Nη so that ε ( N ) ≤δ + ρ−η for all N≥Nη ; then apply Theorem 10.5. The alternative argument follows from Theorem 10.4. Lemma 10.8 (Closure of the certificate under strict exceptional policy).Let r† be the unique class with 3 r† + 1 ≡ 0 ( mod 2 k ). If, at r† , the inequality is enforced with conservative valuation v2 := k and canonical successor Fk ( r† ), then the certificate remains valid and all above lemmas hold unchanged. Proof. At r† the conservative choice increases a ( r† )(i.e. makes the left-hand side larger) relative to any observed valuation k + ∆ with ∆ ≥ 0. Hence the corresponding inequality becomes strictly harder and its satisfaction implies the non-conservative version. All subsequent lemmas depend only on the family of certificate inequalities and therefore remain valid. Remark (Executable status). Each lemma above corresponds to a named fact in the Closure theory: cert_ineq_total_of_OK (Theorem 10.1), finite_phi_image / phi_pairs_nonempty_if_total (Theorem 10.2), phi_min_le_any (Theorem 10.3), V_lower_bound_on_S (Theorem 10.4), and the drift/telescoping and eventuality lemmas (Theorems 10.5 to 10.7). They are structured to be directly executable: the hypotheses are the single predicate verifier_OK plus fixed parameters, and conclusions are algebraic inequalities over reals and naturals, discharged inside Isabelle/HOL without additional oracles. References [1] G. H. Hardy and E. M. Wright, An Introduction to the Theory of Numbers, 6th ed., Oxford Univ. Press, 2008. (Units mod 2k, inverses; basic p-adic valuation laws.) [2] K. Ireland and M. Rosen, A Classical Introduction to Modern Number Theory, 2nd ed., Springer GTM 84, 1990. (p-adic valuations; congruences; lifting arguments.) [3] J. C. Lagarias, “The 3 x +1 problem and its generalizations,” American Mathematical Monthly 92 (1985), 3–23. (Background on accelerated maps and folklore facts.) [4] R. Bellman, Dynamic Programming, Princeton Univ. Press, 1957. (Max-plus/difference constraints viewpoint.) 8 [5] R. M. Karp, “A characterization of the minimum cycle mean in a digraph,” Discrete Mathematics 23 (1978), 309–311. (Cycle-mean feasibility criterion underlying certificates.) [6] N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., SIAM, 2002. (General interval/rounding-control background.) 9