Comparison nodes of the fourth term $3b-2a$

Proved

Erdos195.fourth_term_node

by Ethan Cheung Wang · Oct 23, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmetic-progressionscombinatoricserdos-problems

Let $a\ne b$ be integers, $c=3b-2a$ , $k=\nu_2(b-a)$ . Then: (i) $\nu_2(c-a)=k$ and $\mathrm{bit}_k(c)=\mathrm{bit}_k(b)$ ; (ii) $\nu_2(c-b)=k+1$ and $c\equiv b\pmod{2^{k+1}}$ ; (iii) for $x\ne b$ with $p=\nu_2(b-x)$ and $2^p\mid a-x$ (i.e. $p\le\nu_2(a-x)$ or $x=a$ ):

\nu_2(c-x)=p,\qquad \mathrm{bit}_p(c)=\mathrm{bit}_p(b);

(iv) for $x\ne a$ with $\nu_2(a-x)+1<\nu_2(b-x)$ : $\nu_2(c-x)=\nu_2(a-x)+1$ . Thus the comparison node of the fourth term $c$ with $x$ coincides with that of $b$ whenever $p\le q$ . Used for completing pairs in tree-order constructions (Erdős Problem 195).

Formalization note: treeLt is from Definitions.Def_Erdos195_tree; Safe, bitOne from Definitions.Def_Erdos195_defs; positions are List.idxOf, $\nu_2$ is padicValInt 2.

Preamble

import Mathlib
import Definitions.Def_Erdos195_tree

Formal statement

namespace Erdos195

theorem fourth_term_node (a b : ℤ) (hab : a ≠ b) :
    (padicValInt 2 ((3 * b - 2 * a) - a) = padicValInt 2 (b - a) ∧
      (bitOne (3 * b - 2 * a) (padicValInt 2 (b - a)) ↔ bitOne b (padicValInt 2 (b - a)))) ∧
    (padicValInt 2 ((3 * b - 2 * a) - b) = padicValInt 2 (b - a) + 1 ∧
      (3 * b - 2 * a) % 2 ^ (padicValInt 2 (b - a) + 1) = b % 2 ^ (padicValInt 2 (b - a) + 1)) ∧
    (∀ x : ℤ, x ≠ b → (2 : ℤ) ^ padicValInt 2 (b - x) ∣ a - x →
      padicValInt 2 ((3 * b - 2 * a) - x) = padicValInt 2 (b - x) ∧
      (bitOne (3 * b - 2 * a) (padicValInt 2 (b - x)) ↔ bitOne b (padicValInt 2 (b - x)))) ∧
    (∀ x : ℤ, x ≠ a → padicValInt 2 (a - x) + 1 < padicValInt 2 (b - x) →
      padicValInt 2 ((3 * b - 2 * a) - x) = padicValInt 2 (a - x) + 1) := by sorry

end Erdos195

Source

Erdős Problem 195 (https://www.erdosproblems.com/195); statement from GPT 6 Astra (Oct 23 2026 tree answers), Lean-verified by Grok Bot for Ethan Cheung

View graph

Comparison nodes of the fourth term 3b−2a3b-2a3b−2a

Comparison nodes of the fourth term $3b-2a$