Collatz Map Basics

3.2 Parity Vectors

Definition 84
#
Lean declarations:

A parity vector is a finite sequence of bits (0 and 1). In the formalization, it is represented as a list of boolean values, where false corresponds to 0 and true corresponds to 1.

Definition 85
#
Lean declarations:

For a parity vector \(v\), \(q(v)\) is the number of ones (true entries) in \(v\).

Definition 86
#
Lean declarations:

The size of a parity vector \(v\), denoted \(|v|\), is its length.

Definition 87
#
Lean declarations:

The ones-ratio of a parity vector \(v\) is the rational number \(q(v) / |v|\). If the vector is empty, the ratio is defined to be 0.

Definition 88
#
Lean declarations:

For \(j, n \in \mathbb {N}\), the parity vector \(V(j, n)\) of length \(j\) for the compact Collatz sequence starting at \(n\) is defined as

\[ V(j, n) = (X(n), X(T(n)), \dots , X(T^{j-1}(n))). \]
Lemma 89
#
Lean declarations:

The length of \(V(j, n)\) is \(j\).

Proof

Immediate from the definition.

Lemma 90
#
Lean declarations:

For any \(i {\lt} j\), the \(i\)-th entry of \(V(j, n)\) is \(X(T^i(n))\).

Proof

Immediate from the definition.

Definition 91
#
Lean declarations:

The elementary precedence relation \(\prec _e\) is defined by swapping a \(01\) subword with \(10\):

\begin{equation} w_1 01 w_2 \prec _e w_1 10 w_2. \end{equation}
3

The precedence relation \(\preceq \) is the reflexive transitive closure of \(\prec _e\).

Definition 92
#
Lean declarations:

For \(k, n \in \mathbb {N}\), the vector \(E(k, n)\) is the function from \(\{ 0, \dots , k-1\} \) to \(\{ 0, 1\} \) defined by

\begin{equation} E(k, n)(i) = X(T^i(n)). \end{equation}
4

Lemma 93
#
Lean declarations:

Each entry of \(E(k, n)\) is at most 1.

Proof

Immediate from the definition of \(X(n)\).

Lemma 94

The number of odd steps \(Q(k, n)\) is equal to the sum of the entries of \(E(k, n)\):

\begin{equation} Q(k, n) = \sum _{i=0}^{k-1} E(k, n)(i). \end{equation}
5

Proof

By definition of \(Q(k, n)\) and \(E(k, n)\).

Lemma 95

If \(E(k+1, m) = E(k+1, n)\), then \(E(k, m) = E(k, n)\).

Proof

The agreement on the first \(k+1\) entries implies agreement on the first \(k\) entries.

Lemma 96

If \(E(k, m) = E(k, n)\), then \(Q(k, m) = Q(k, n)\).

Proof

Directly from Lemma 94.