Infinite case of red diamond conjecture

Stream: new members

[Michael Bucko]

I formalized the connectedness of the red sequence without the lookup table (ie. the finite case was quickly proven by @Daniel Weber , but in the more general case the matrix won't be used anymore (it was finite and would not give me the whole sequence)).

image.png

The code is still new, so it could have bugs (the other one was very stable, but could not be used for the infinite case). In case of bugs: the intention here is to make sure that for every (red seq) number of the form $3^{k+1}$ in row $r+1$ in the table, the previous number in the red sequence is in row $r$ and column $k$.

import Mathlib

def is_k_almost_prime (k n : Nat) : Bool :=
  n > 1 && n.factorization.sum (fun _ multiplicity => multiplicity) == k

def is_k_almost_prime_prop (k n : Nat) : Prop :=
  is_k_almost_prime k n = true

noncomputable def nth_k_almost_prime (k i : Nat) : Nat :=
  Classical.epsilon (fun n =>
    is_k_almost_prime_prop k n ∧
    (((List.range (n+1)).filter (is_k_almost_prime k)).length = i+1)
  )

noncomputable def almost_prime_table (k i : Nat) : Nat :=
  nth_k_almost_prime (k+1) i

def col_has_power (k power : Nat) : Prop :=
  ∃ i, almost_prime_table k i = power

noncomputable instance (k power : Nat) : Decidable (col_has_power k power) :=
  Classical.propDecidable _

noncomputable def find_power_index (k power : Nat) : Option Nat :=
  if h : col_has_power k power then
    some (Nat.find h)
  else
    none

noncomputable def red_diamond_sequence_column (k : Nat) : Set Nat :=
  let currentPower := 3^(k+1)
  let nextPower := 3^(k+2)
  match find_power_index (k+1) nextPower with
  | some r => { n | n ≥ currentPower ∧ ∃ i, i < r ∧ almost_prime_table k i = n }
  | none   => { n | n ≥ currentPower ∧ ∃ i, almost_prime_table k i = n }

lemma red_diamond_conjecture_infinite : ∀ k,
  (∀ r, find_power_index (k+1) (3^(k+2)) = some r →
    almost_prime_table (k+1) r = 3^(k+2) ∧
    (∀ i, i < r → almost_prime_table k i ∈ red_diamond_sequence_column k)) := by
  sorry

For the reference, I start proving like this

  intro k
  intros r h_find
  unfold find_power_index at h_find
  have h_col_has_power : col_has_power (k+1) (3^(k+2)) :=
    by