Böhm-Sontacchi Cycle Equation

If n is periodic under the Collatz function with period p, i.e. collatz^[p] n = n, then the iterate formula specializes to 2^a · n = 3^b · n + c, which rearranges to (2^a - 3^b) · n = c in the integers. This is the fundamental arithmetic constraint on Collatz cycles.

theorem Collatz.cycle_linear_constraint {n p : ℕ} (hcyc : collatz^[p] n = n) : ∃ (a : ℕ) (b : ℕ) (c : ℕ), a + b = p ∧ 2 ^ a * n = 3 ^ b * n + c

theorem Collatz.cycle_equation_int {n p : ℕ} (hcyc : collatz^[p] n = n) : ∃ (a : ℕ) (b : ℕ) (c : ℕ), a + b = p ∧ (2 ^ a - 3 ^ b) * ↑n = ↑c

theorem Collatz.cycle_two_pow_ge {n p : ℕ} (hn : 0 < n) (hcyc : collatz^[p] n = n) : ∃ (a : ℕ) (b : ℕ) (c : ℕ), a + b = p ∧ 2 ^ a * n = 3 ^ b * n + c ∧ 3 ^ b ≤ 2 ^ a