# User:Hakerh400/Proof 002

This is a proof that the algorithm described in User:Hakerh400/Bijection between reals and the powerset of naturals is incorrect. In particular, real number ${\displaystyle -0.75}$ cannot be represented as a sequence of binary digits using the algorithm.

### Definitions

A bit is either ${\displaystyle 0}$ or ${\displaystyle 1}$.

A natural number is either zero, or a successor of a natural number.

A real number is a 3-tuple ${\displaystyle (S,N,F)}$ where ${\displaystyle S}$ is a bit, ${\displaystyle N}$ is a natural number and ${\displaystyle F}$ is a countably infinite sequence of bits. There are two constraints:

• ${\displaystyle F}$ does not end with infinitely many ${\displaystyle 1}$s (for each natural number ${\displaystyle n}$, there exists a natural number ${\displaystyle k\geq n}$ such that ${\displaystyle k}$-th bit of ${\displaystyle F}$ is ${\displaystyle 0}$).
• If ${\displaystyle F}$ consists only of ${\displaystyle 0}$s and ${\displaystyle N}$ is zero, then ${\displaystyle S}$ is ${\displaystyle 0}$.

Informally, ${\displaystyle S}$ represents the sign of the real number (${\displaystyle 0}$ - nonnegative, ${\displaystyle 1}$ - negative), ${\displaystyle N}$ represents the absolute value of the integral part, ${\displaystyle F}$ represents the binary expansion of the fractional part.

Referencing bits in sequences of bits is 0-indexed.

Function `bits_to_real` maps countably infinite sequences of bits to real numbers. It is defined in the following way. Given sequence of bits ${\displaystyle f}$. There are two cases:

• ${\displaystyle f}$ ends with infnitely many same bits. ${\displaystyle S}$ is that bit. Let ${\displaystyle i}$ be the index of the first of the ending bits (the first index such that from that index on, all bits are equal to that bit). Let ${\displaystyle f'}$ be ${\displaystyle f}$ with all bits starting from ${\displaystyle i+1}$ replaced with ${\displaystyle 0}$. ${\displaystyle N}$ is the index of the first ${\displaystyle 0}$ in ${\displaystyle f'}$. ${\displaystyle F}$ is ${\displaystyle f'}$ without the first ${\displaystyle N+1}$ bits.
• ${\displaystyle f}$ does not end with infinitely many same bits. ${\displaystyle S}$ is the first bit. Let ${\displaystyle f'}$ be ${\displaystyle f}$ without the first bit. ${\displaystyle N}$ is the index of the first ${\displaystyle 0}$ in ${\displaystyle f'}$. ${\displaystyle F}$ is ${\displaystyle f'}$ without the first ${\displaystyle N+1}$ bits.

### Theorem

Function `bits_to_real` between countably infinite sequences of bits and real numbers in injective, but not surjective, and therefore not bijective.

### Proof

```-- Lean: v3.35.1
-- Mathlib: d856bf9b

import tactic
import data.nat.lattice

open nat
open function
open classical

open_locale classical

namespace real

noncomputable theory

def ends_with (b : Prop) (f : ℕ → Prop) : Prop :=
∃ (i : ℕ), ∀ {n : ℕ}, i ≤ n → f n = b

structure Real :=
(neg : Prop)
(n : ℕ)
(f : ℕ → Prop)
(h₁ : ¬ends_with true f)
(h₂ : (∀ (n : ℕ), ¬f n) → n = 0 → ¬neg)

def slice (k : ℕ) (f : ℕ → Prop) (n : ℕ) : Prop :=
f (n + k)

class preserves_end (F : (ℕ → Prop) → ℕ → Prop) : Prop :=
(pe: ∀ {f : ℕ → Prop} {b : Prop}, ends_with b (F f) = ends_with b f)

lemma pr_end {F : (ℕ → Prop) → ℕ → Prop} [preserves_end F] :
∀ {f : ℕ → Prop} {b : Prop}, ends_with b (F f) = ends_with b f
:= by apply preserves_end.pe

instance {k : ℕ} : preserves_end (slice k) := begin
split, rintro f b, ext, split; rintro ⟨i, h⟩,
{ use i + k, rintro n h₁,
obtain ⟨n, rfl⟩ := exists_eq_add_of_le h₁, clear h₁,
apply h, apply le_add_right (le_refl _) },
{ use i, rintro n h₁, apply h, apply le_add_right h₁ },
end

def n_aux (f : ℕ → Prop) : ℕ := Inf {i | ¬f i}

def get_nf (f : ℕ → Prop) : ℕ × (ℕ → Prop) :=
⟨n_aux f, slice (n_aux f + 1) f⟩

def real_from_nf
(neg : Prop)
(snf : ℕ × (ℕ → Prop))
(h₁ : ¬ends_with true snf.2)
(h₂ : (∀ (n : ℕ), ¬snf.2 n) → snf.1 = 0 → ¬neg)
: Real := ⟨neg, snf.1, snf.2, h₁, h₂⟩

def min_end (b : Prop) (f : ℕ → Prop) : ℕ :=
Inf {i | ∀ (n : ℕ), i ≤ n → f n = b }

def bits_to_real (f : ℕ → Prop) : Real :=
if h : ∃ {b : Prop}, ends_with b f
then real_from_nf (some h) (get_nf
(λn, n < min_end (some h) f + 1 ∧ f n))
begin
simp_rw [ends_with, get_nf, slice],
generalize_proofs, push_neg, intro i,
use max i (min_end (some h) f + 1), split,
{ apply le_max_left },
{ rw [ne, eq_true], apply not_and_of_not_left,
push_neg, apply le_add_right, apply le_max_right },
end
begin
intro F_all_0s,
intro N_is_0,
intro h₁,
revert F_all_0s N_is_0,
have f_ends_with_1s := some_spec h,
rw ←@eq_true (some h) at h₁, rw h₁ at *, clear h₁,
generalize f'_def : (λ (n : ℕ), n < min_end true f + 1 ∧ f n) = f',
generalize F_def : (get_nf f').snd = F,
intro F_all_0s,
intro N_is_0,
have f'_ends_with_0s : ends_with false f',
{ use min_end true f + 1, rintro i h₁,
rw ←f'_def, dsimp only, rw eq_false,
apply not_and_of_not_left, push_neg, exact h₁ },
have f'_has_0 : ∃ (n : ℕ), ¬f' n,
{ obtain ⟨n, h₁⟩ := f'_ends_with_0s, use n,
replace h₁ := @h₁ n (le_refl _),
rw eq_false at h₁, exact h₁ },
have f'_0_is_0 : ¬f' 0,
{ simp_rw [get_nf, n_aux, Inf] at N_is_0,
split_ifs at N_is_0 with h₁,
{ letI := prop_decidable,
exact (nat.find_eq_zero f'_has_0).mp N_is_0 },
{ obtain ⟨n, h₂⟩ := f'_has_0,
push_neg at h₁, exfalso, exact h₁ n h₂ }},
have f'_has_1 : ∃ (n : ℕ), f' n,
{ rw ←f'_def, use min_end true f, split,
{ apply lt_succ_self },
{ simp_rw [min_end, Inf], split_ifs with h₁,
{ exact eq_true.mp (nat.find_spec f_ends_with_1s (le_refl _)) },
{ obtain ⟨i, h₂⟩ := id f_ends_with_1s,
exfalso, push_neg at h₁, apply h₁ i, assumption }}},
have F_is_slice_1_f' : F = slice 1 f',
{ have h₁ := le_zero_iff.mp (@nat.Inf_le {i : ℕ | ¬f' i} _ f'_0_is_0),
ext n, simp_rw [←F_def, get_nf, n_aux, h₁] },
have F_has_1 : ∃ (n : ℕ), F n,
{ obtain ⟨n, h₁⟩ := f'_has_1, cases n,
{ exfalso, exact f'_0_is_0 h₁, },
{ use n, simp_rw [F_is_slice_1_f', slice], exact h₁ } },
exact F_all_0s _ (some_spec F_has_1),
end
else real_from_nf (f 0) (get_nf (slice 1 f))
begin
push_neg at h, replace h := @h true,
simp_rw [get_nf, pr_end], exact h,
end
begin
push_neg at h, replace h := @h false,
simp_rw [get_nf, n_aux],
rintro h₁ h₂,
rw [h₂, zero_add] at h₁, clear h₂,
unfold slice at h₁,
unfold ends_with at h,
push_neg at h, exfalso,
obtain ⟨n, ⟨h₁, h₂⟩⟩ := h 2, clear h,
obtain ⟨n, rfl⟩ := exists_eq_add_of_lt h₁, clear h₁,
rw [ne, eq_false, add_comm 1 n] at h₂,
exact h₂ (h₁ n),
end

lemma exi_end_iff {f : ℕ → Prop} :
(∃ (b : Prop), ends_with b f) ↔
(∃ (b : Prop), ends_with b (bits_to_real f).f) :=
begin
split; intro h,
{ use false,
simp_rw [bits_to_real, real_from_nf, get_nf],
split_ifs with h₁,
{ clear h₁,
generalize h₁ : n_aux
(λ (n : ℕ), n < min_end (some h) f + 1 ∧ f n) + 1 = k₁,
generalize h₂ : min_end (some h) f + 1 = k₂,
use k₂, rintro n h₃, rw [eq_false, slice],
apply not_and_of_not_left, push_neg,
{ simp_rw [bits_to_real, real_from_nf, get_nf] at h,
split_ifs at h with h₁,
{ exact h₁ },
{ simp_rw [pr_end] at h, contradiction }},
end

lemma eq_slice {f₁ f₂ : ℕ → Prop} (n : ℕ) :
((∀ (k : ℕ), k < n → f₁ k = f₂ k) ∧
slice n f₁ = slice n f₂) ↔ f₁ = f₂ :=
begin
split,
{ rintro ⟨h₁, h₂⟩, ext i,
by_cases h₃ : i < n,
{ exact iff_of_eq (h₁ i h₃) },
{ push_neg at h₃,
obtain ⟨i, rfl⟩ := exists_eq_add_of_le h₃,
replace h₂ := congr_fun h₂ i,
unfold slice at h₂, rw add_comm at h₂,
exact iff_of_eq h₂ }},
{ intro h, subst h, split,
{ rintro k h, refl },
{ refl }},
end

lemma exi_bit {f : ℕ → Prop}
(h : ∀ (b : Prop), ¬ends_with b f) :
∀ (b : Prop), ∃ (n : ℕ), f n = b :=
begin
intro b,
replace h := h ¬b,
unfold ends_with at h,
push_neg at h,
obtain ⟨i, ⟨h₁, h₂⟩⟩ := h 0,
use i, ext, tauto,
end

lemma exi_bit_slice {f : ℕ → Prop}
(h : ∀ (b : Prop), ¬ends_with b f) :
∀ (b : Prop) (k : ℕ), ∃ (n : ℕ), slice k f n = b :=
begin
rintro b k, unfold slice, apply exi_bit,
clear b, intro b, replace h := h b,
have h₁ := id h, rw ←@pr_end (slice k) at h₁, exact h₁,
end

lemma eq_of_n_aux {f₁ f₂ : ℕ → Prop}
(h₄ : n_aux f₁ = n_aux f₂)
(h₅ : slice (n_aux f₁ + 1) f₁ = slice (n_aux f₂ + 1) f₂)
(h₁ : ∃ (n : ℕ), ¬f₁ n)
(h₂ : ∃ (n : ℕ), ¬f₂ n) :
f₁ = f₂ :=
begin
rw h₄ at h₅,
refine (eq_slice _).mp ⟨_, h₅⟩,
rintro k h₆,
replace h₆ := le_of_lt_succ h₆,
rw [n_aux] at h₆,
replace h₆ := le_iff_eq_or_lt.mp h₆,
cases h₆,
{ have h₇ := h₆,
unfold n_aux at h₄,
rw ←h₄ at h₆,
have h₈ := @nat.Inf_mem (λk, ¬f₁ k) h₁,
have h₉ := @nat.Inf_mem (λk, ¬f₂ k) h₂,
simp_rw ←eq_false at h₆ h₇ h₈ h₉,
transitivity false,
{ rw h₆, exact h₈ },
{ rw h₇, exact eq.symm h₉ }},
{ have h₇ := h₆, unfold n_aux at h₄, rw ←h₄ at h₆,
replace h₆ := not_not.mp (nat.not_mem_of_lt_Inf h₆),
replace h₇ := not_not.mp (nat.not_mem_of_lt_Inf h₇),
ext, tauto },
end

lemma min_end_eq {f : ℕ → Prop} {b : Prop}
(h₁ : ends_with b f) :
∀ (k : ℕ), min_end b f ≤ k → f k = b :=
by rintro k h₂; exact @nat.Inf_mem _ h₁ k h₂

lemma m_wlog {f₁ f₂ : ℕ → Prop}
(h' : bits_to_real f₁ = bits_to_real f₂)
(h₁ : ∃ {b : Prop}, ends_with b f₁)
(h₂ : ∃ {b : Prop}, ends_with b f₂) :
let b : Prop := some h₁,
m₁ : ℕ := min_end b f₁,
m₂ : ℕ := min_end b f₂,
F₁ : ℕ → Prop := λ (n : ℕ), n < m₁ + 1 ∧ f₁ n,
F₂ : ℕ → Prop := λ (n : ℕ), n < m₂ + 1 ∧ f₂ n
in b = some h₂ →
ends_with b f₁ →
ends_with b f₂ →
n_aux F₁ = n_aux F₂ →
(∀ (a : ℕ), F₁ a = F₂ a) →
(∀ (a : ℕ),
F₁ (a + (n_aux F₁ + 1)) = F₂ (a + (n_aux F₂ + 1))) →
m₁ ≤ m₂ :=
begin
intros b m₁ m₂ F₁ F₂ h₃ h₆ h₇ h₄ h₈ h₅,
by_contra hm, push_neg at hm,
by_cases hb : b,
{ rw ←@eq_true b at hb, rw hb at *,
have hm₁ : ∀ (k : ℕ), m₁ < k → ¬F₁ k,
{ rintro k hk, simp_rw F₁, apply not_and_of_not_left,
push_neg, apply succ_le_of_lt hk },
have hm₂ : ∀ (k : ℕ), m₂ < k → ¬F₂ k,
{ rintro k hk, simp_rw F₂, apply not_and_of_not_left,
push_neg, apply succ_le_of_lt hk },
have hx : F₁ m₁,
{ simp_rw F₁, refine ⟨lt_succ_self _, _⟩,
rw ←@eq_true (f₁ m₁), simp_rw [m₁, min_end, b],
apply nat.Inf_mem h₆, simp_rw [←b, hb], apply le_refl },
have hy : ¬F₂ m₁,
{ simp_rw F₂,
apply not_and_of_not_left,
push_neg,
apply succ_le_of_lt hm },
rw ←h₈ at hy, contradiction },
{ obtain ⟨d, hd⟩ := exists_eq_add_of_lt hm,
rw ←eq_false at hb, rw hb at *,
have hm₁ : ∀ (k : ℕ), m₁ ≤ k → ¬f₁ k,
{ rintro k hk,
simp_rw [m₁, min_end, hb] at hk,
exact eq_false.mp (@nat.Inf_mem _ h₆ _ hk) },
have hx : F₁ (pred m₁),
{ have hm₂ : m₂ + d < m₁,
{ rw hd, apply lt_succ_self },
simp_rw [m₁, min_end] at hm₂,
have hm₃ : ¬∀ (n : ℕ), m₂ + d ≤ n → f₁ n = b,
{ exact nat.not_mem_of_lt_Inf hm₂ },
push_neg at hm₃,
simp_rw [hb, ne, eq_false, not_not] at hm₃,
simp_rw [F₁, hd, pred],
obtain ⟨n, ⟨hn₁, hn₂⟩⟩ := hm₃,
split,
{ apply lt_succ_of_lt, apply lt_succ_self },
{ cases hn₁ with n hn₃,
{ exact hn₂ },
{ exfalso,
refine hm₁ _ _ hn₂,
rw hd,
exact hn₃ }}},
have hy : ¬F₂ (pred m₁),
{ simp_rw [F₂, hd, pred],
apply not_and_of_not_right,
simp_rw ←eq_false,
apply nat.Inf_mem h₇,
simp_rw [m₂, min_end, hb],
rw ←h₈ at hy, contradiction },
end

lemma inj_bits_to_real : injective bits_to_real := begin
rintro f₁ f₂ h,
have h' := h,
simp_rw [bits_to_real, real_from_nf, get_nf] at h,
split_ifs at h with h₁ h₂ h₂,
{ rcases h with ⟨h₃, ⟨h₄, h₅⟩⟩,
have h₆ := some_spec h₁,
have h₇ := some_spec h₂,
rw ←h₃ at *,
have h₈ := eq_of_n_aux h₄ h₅ begin
use min_end (some h₁) f₁ + 2,
apply not_and_of_not_left,
push_neg, apply le_succ,
end
begin
use min_end (some h₁) f₂ + 2,
apply not_and_of_not_left,
push_neg, apply le_succ,
end,
have h₉ : min_end (some h₁) f₁ = min_end (some h₁) f₂,
{ revert h₃ h₄ h₅ h₆ h₇ h₈,
generalize b_def : some h₁ = b,
generalize m₁_def : min_end b f₁ = m₁,
generalize m₂_def : min_end b f₂ = m₂,
generalize F₁_def : (λ (n : ℕ), n < m₁ + 1 ∧ f₁ n) = F₁,
generalize F₂_def : (λ (n : ℕ), n < m₂ + 1 ∧ f₂ n) = F₂,
rintro h₃ h₄ h₅ h₆ h₇ h₈,
replace h₅ := congr_fun h₅,
replace h₈ := congr_fun h₈,
unfold slice at h₅,
apply le_antisymm,
{ subst_vars, apply m_wlog; assumption },
{ subst h₃,
subst_vars, apply m_wlog;
try {try {symmetry}, assumption},
{ intro a, exact eq.symm (h₈ a) },
{ intro a, exact eq.symm (h₅ a) }}},
replace h₈ := congr_fun h₈, dsimp at h₈,
rw ←h₉ at h₈,
apply (eq_slice (min_end (some h₁) f₁ + 1)).mp, split,
{ rintro k h₁₀, ext, split; intro h,
{ exact ((iff_of_eq (h₈ k)).mp ⟨h₁₀, h⟩).2 },
{ exact ((iff_of_eq (h₈ k)).mpr ⟨h₁₀, h⟩).2 }},
{ apply funext, intro n, unfold slice,
transitivity some h₁,
{ apply min_end_eq,
{ exact h₆ },
{ exact le_add_left (le_succ _) }},
{ symmetry, apply min_end_eq,
{ rw h₃, exact some_spec h₂ },
{ rw ←h₉, exact le_add_left (le_succ _) }}}},
{ rw exi_end_iff at h₁ h₂, rw h' at h₁, contradiction },
{ rw exi_end_iff at h₁ h₂, rw h' at h₁, contradiction },
{ push_neg at h₁ h₂,
rcases h with ⟨h₃, ⟨h₄, h₅⟩⟩,
apply (eq_slice 1).mp, split,
{ rintro k h₆, rw [lt_one_iff.mp h₆, h₃] },
{ apply eq_of_n_aux h₄ h₅; simp_rw ←eq_false;
apply exi_bit_slice _ false 1; assumption }},
end

lemma not_surj_bits_to_real : ¬surjective bits_to_real := begin
rintro surj,
generalize F_def : (λ (n : ℕ), n < 2) = F,
obtain ⟨f, h₁⟩ := surj
{ neg := true,
n := 0,
f := F,
h₁ := begin
unfold ends_with,
push_neg,
rintro i,
use max i 2,
refine ⟨le_max_left _ _, _⟩,
rw [ne, eq_true],
subst F_def,
dsimp,
push_neg,
apply le_max_right,
end,
h₂ := begin
rintro h₁ h₂,
clear h₂,
exfalso,
subst F_def,
replace h₁ := h₁ 0,
dsimp at h₁,
push_neg at h₁,
exact absurd h₁ (not_succ_le_zero _),
end },
have hf₁ := (@exi_end_iff F).mp begin
use false,
subst F_def,
use 2,
rintro n hn,
dsimp,
rw eq_false,
push_neg,
assumption,
end,
simp_rw [bits_to_real, real_from_nf, get_nf] at h₁,
split_ifs at h₁ with hi₁,
{ rcases h₁ with ⟨h₁, ⟨h₂, h₃⟩⟩,
simp_rw h₁ at h₂ h₃,
subst F_def,
generalize m_def : min_end true f = m,
clear hf₁,
simp_rw m_def at h₂ h₃,
replace h₃ : ∀ (n : ℕ), n < 2 ↔ n < m ∧ f (n + 1),
{ replace h₃ := congr_fun h₃,
simp_rw slice at h₃,
dsimp at h₃,
rintro n,
replace h₃ := h₃ n,
symmetry' at h₃,
exact iff_of_eq h₃ },
have f_ends_with_1s : ends_with true f,
{ have h := some_spec hi₁,
rw h₁ at h,
exact h },
have f_0_eq_0 : ¬f 0,
{ simp_rw [n_aux, Inf] at h₂,
split_ifs at h₂,
{ rw nat.find_eq_iff at h₂,
replace h₂ := h₂.1,
dsimp at h₂,
contrapose h₂,
push_neg at h₂ ⊢,
exact ⟨zero_lt_succ _, h₂⟩ },
{ exfalso,
push_neg at h,
replace h := h (m + 1),
dsimp at h,
push_neg at h,
exact lt_irrefl _ h.1 }},
have min_end_ne_zero : m ≠ 0,
{ simp_rw min_end at m_def,
have hm := nat.Inf_mem f_ends_with_1s (le_refl _),
rw eq_true at hm,
intro h, subst h,
change f (Inf {i : ℕ | ∀ (n : ℕ), i ≤ n → f n = true}) at hm,
rw m_def at hm,
obtain ⟨x, hx⟩ := exists_eq_succ_of_ne_zero min_end_ne_zero,
have f_x_succ_eq_1 : f x.succ,
{ simp_rw min_end at m_def,
have hm := nat.Inf_mem f_ends_with_1s (le_refl _),
rw [←hx, ←m_def],
rw eq_true at hm,
assumption },
have min_end_ge_2 : 2 < m,
{ have h₄ : f 1 := ((h₃ 0).mp (zero_lt_succ _)).2,
have h₅ : 1 < m := ((h₃ 1).mp (lt_succ_self _)).1,
replace h₅ : 2 ≤ m := succ_le_of_lt h₅,
rw le_iff_eq_or_lt at h₅,
cases h₅,
{ exfalso,
subst h₅,
replace hx := succ.inj hx,
subst hx,
have he : ∀ (n : ℕ), 2 ≤ n → f n = true,
{ simp_rw [min_end, Inf] at m_def,
split_ifs at m_def;
rw nat.find_eq_iff at m_def; exact m_def.1 },
have h : min_end true f = 1,
{ simp_rw [min_end, Inf],
split_ifs,
{ rw nat.find_eq_iff,
dsimp,
split,
{ rintro n hn,
rw le_iff_eq_or_lt at hn,
cases hn,
{ rw eq_true,
subst hn,
assumption },
{ apply he _ (succ_le_of_lt hn) }},
{ rintro n hn,
rw lt_one_iff at hn,
subst hn,
push_neg,
use 0,
refine ⟨le_refl _, _⟩,
rw [ne, eq_true],
assumption }},
{ exfalso,
contrapose h,
push_neg,
use 2,
assumption }},
{ linarith }},
{ assumption }},
have not_x_lt_2 : ¬x < 2,
{ subst hx,
push_neg,
apply le_of_lt_succ,
assumption },
rw ←eq_false at not_x_lt_2,
have h₄ := (h₃ x).mpr,
rw not_x_lt_2 at h₄,
change ¬(x < m ∧ f x.succ) at h₄,
push_neg at h₄,
rw hx at h₄,
replace h₄ := h₄ (lt_succ_self _),