The reverse binary order

This file formalizes the order ◁ introduced before Lemma 1 in the paper “A 4AP-free permutation of the positive integers”. The least significant unequal bit decides the comparison, with 1 preceding 0. Dividing by two removes a common least significant bit. We use this recursive description both for a computable comparison and for the elementary proofs in the paper.

@[irreducible]

def FourAP.binaryCompare (a b : ℕ) : Bool

The binary comparison from the paragraph defining ◁ in the paper. It returns true precisely when the first argument precedes the second. The special case (0, 0) ends the recursion after all bits have been removed.

Equations

• FourAP.binaryCompare a b = if a + b = 0 then false else if a % 2 = b % 2 then FourAP.binaryCompare (a / 2) (b / 2) else decide (b % 2 < a % 2)

def FourAP.bits (a b : ℕ) : Prop

The paper's strict order ◁, the reverse order on binary strings when compared at their first unequal bit starting from the least significant end.

Equations

• FourAP.bits a b = (FourAP.binaryCompare a b = true)

@[instance_reducible]

instance FourAP.bitsDecidable : DecidableRel bits

Binary comparison is decidable by the recursion defining the paper's order.

Equations

• FourAP.bitsDecidable x✝¹ x✝ = FourAP.bitsDecidable._aux_1 x✝¹ x✝

@[simp]

theorem FourAP.not_bits_zero_zero : ¬bits 0 0

At equal zero strings, there is no first unequal bit.

theorem FourAP.bits_iff (a b : ℕ) : bits a b ↔ b % 2 < a % 2 ∨ a % 2 = b % 2 ∧ bits (a / 2) (b / 2)

Recursive form of the paper's definition: compare the low bits first, then discard them if they agree.

theorem FourAP.bits_iff_of_same_parity {a b : ℕ} (hp : a % 2 = b % 2) : bits a b ↔ bits (a / 2) (b / 2)

Equal parity allows the rescaling described in the self-similarity paragraph of the paper.

theorem FourAP.bits_iff_of_diff_parity {a b : ℕ} (hp : a % 2 ≠ b % 2) : bits a b ↔ b % 2 < a % 2

For unequal parity, the least significant bit already decides the order.

@[simp]

theorem FourAP.bits_even_even (a b : ℕ) : bits (2 * a) (2 * b) ↔ bits a b

Self-similarity of ◁ on the even integers (before Lemma 1).

@[simp]

theorem FourAP.bits_odd_odd (a b : ℕ) : bits (2 * a + 1) (2 * b + 1) ↔ bits a b

Self-similarity of ◁ on the odd integers (before Lemma 1).

theorem FourAP.bits_parity (a b p : ℕ) (hp : p < 2) : bits (2 * a + p) (2 * b + p) ↔ bits a b

The two parity restrictions have the same rescaled order, as used in Lemma 2. Here p = 0 selects the even part and p = 1 the odd part.

theorem FourAP.bits_odd_even (a b : ℕ) : bits (2 * a + 1) (2 * b)

All odd integers precede all even integers (the self-similarity paragraph).

theorem FourAP.not_bits_even_odd (a b : ℕ) : ¬bits (2 * a) (2 * b + 1)

The converse parity comparison never holds.

theorem FourAP.bits_irrefl (a : ℕ) : ¬bits a a

Irreflexivity verifies that the paper's binary comparison is strict.

theorem FourAP.bits_ne {a b : ℕ} (h : bits a b) : a ≠ b

Two entries compared strictly in ◁ are different.

theorem FourAP.bits_asymm {a b : ℕ} (hab : bits a b) : ¬bits b a

Asymmetry is part of the verification that ◁ is a strict linear order.

theorem FourAP.bits_total {a b : ℕ} (hne : a ≠ b) : bits a b ∨ bits b a

Any distinct binary strings have a first unequal bit: totality of ◁.

theorem FourAP.bits_trans {a b c : ℕ} (hab : bits a b) (hbc : bits b c) : bits a c

Transitivity completes the elementary verification that the binary comparison in the paper defines a strict linear order.

theorem FourAP.not_bits_zero (a : ℕ) : ¬bits 0 a

Zero cannot precede any integer, as asserted just before the discussion of the literature in the paper.

theorem FourAP.bits_zero {a : ℕ} (ha : a ≠ 0) : bits a 0

Zero is the greatest element of ◁ (used in Lemma 2's base case).

theorem FourAP.bits_no_three_of_eq {a b c : ℕ} (hap : a + c = 2 * b) : ¬(bits a b ∧ bits b c)

The elementary 3AP-freeness proof preceding equation (1). If the low bits agree we divide all entries by two; otherwise the middle low bit differs from both endpoint low bits, and two consecutive comparisons are impossible. The equations include increasing and decreasing progressions alike.

theorem FourAP.bits_dual_no_three {a b c : ℕ} (hap : a + c = 2 * b) : ¬(bits b a ∧ bits c b)

The dual order also contains no 3AP, as used in Lemma 1.

theorem FourAP.bits_pairs_of_eq {a b c d : ℕ} (h₁ : a + c = 2 * b) (h₂ : b + d = 2 * c) : bits a b ↔ bits c d

Equation (1), labelled eq:pairs in the paper, in equation form. For four consecutive AP terms, the first and third adjacent pairs compare in the same direction. The proof removes common low bits until parity differs.

theorem FourAP.bits_pairs {a b c d : ℕ} (hap : IsAP4 a b c d) : bits a b ↔ bits c d

Equation (1) of the paper, packaged for a nonconstant four-term AP.

theorem FourAP.bits_apFree : APFree bits

In particular the binary order itself is 4AP-free; this starts the construction with the empty safe prefix.

theorem FourAP.testBit_zero_eq_iff (a b : ℕ) : a.testBit 0 = b.testBit 0 ↔ a % 2 = b % 2

Equality of the lowest binary digits is equality of parity. This is the bridge between the recursive definition and the binary-digit description in the paper.

theorem FourAP.exists_first_differing_bit {a b : ℕ} (hab : bits a b) : ∃ (k : ℕ), (∀ (i : ℕ), i < k → a.testBit i = b.testBit i) ∧ a.testBit k = true ∧ b.testBit k = false

A strict binary comparison exhibits the first unequal bit, with the first integer's bit equal to one and the second integer's bit equal to zero. This is the forward direction of the paper's defining description of ◁.

theorem FourAP.bits_of_first_differing_bit {a b k : ℕ} (hlow : ∀ (i : ℕ), i < k → a.testBit i = b.testBit i) (ha : a.testBit k = true) (hb : b.testBit k = false) : bits a b

Conversely, the least significant unequal bit determines the recursive comparison. This is the backward direction of the paper's definition.

theorem FourAP.bits_iff_first_differing_bit (a b : ℕ) : bits a b ↔ ∃ (k : ℕ), (∀ (i : ℕ), i < k → a.testBit i = b.testBit i) ∧ a.testBit k = true ∧ b.testBit k = false

The definition of ◁ in the paper, stated literally using binary digits. There is a first differing digit, and its values are respectively 1 and 0. Thus our executable recursion is exactly the order described in the text.

theorem FourAP.bits_eight_example : List.Pairwise bits [7, 3, 5, 1, 6, 2, 4, 0]

The displayed eight-element example from the paper: 7 ◁ 3 ◁ 5 ◁ 1 ◁ 6 ◁ 2 ◁ 4 ◁ 0. Pairwise records every comparison in this finite ordered list.