Positive naturals factor into a power of three and a unit

Proved

CollatzWork.residueAncestor_factor_unit

by Sodelin · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

collatz-work-import

For every natural $n>0$ ,

\exists e,u\in\mathbb N,\quad u>0,\quad u\not\equiv0\pmod3,\quad3^e u=n.

This existence lemma supplies the normalized factorization needed by the divisibility-form ancestor theorem.

Preamble

import Std
import Init.Grind.Ordered.Module

Formal statement

theorem CollatzWork.residueAncestor_factor_unit (n : Nat) :
    0 < n → ∃ e u : Nat, 0 < u ∧ u % 3 ≠ 0 ∧ 3 ^ e * u = n := by sorry

Source