FormalConjectures.OEIS.«114137»

/-
Copyright 2026 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/

import FormalConjecturesUtil

Difference between first odd semiprime $> 2^n$ and $2^n$

References:

A114137

namespace OeisA114137open Nat

The primary defining sequence a. $a(n)$ is the difference between first odd semiprime > $2^n$ and $2^n$. $$a(n) = \min {s \mid s > 2^n \text{ and } s \text{ is an odd semiprime}} - 2^n$$

noncomputable def a (n : ℕ) : ℕ :=
  let m := 2^n
  let s : Set ℕ := { s | s > m ∧ s.IsSemiprime ∧ Odd s }
  sInf s - m



@[category API, AMS 11]
lemma a_eq_of (n val : ℕ)
  (h_mem : val.IsSemiprime ∧ Odd val)
  (h_gt : 2^n < val)
  (h_min : ∀ x, 2^n < x → x < val → ¬ (x.IsSemiprime ∧ Odd x)) :
  a n = val - 2^n := byn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ a n = val - 2 ^ n
  change sInf { s | s > 2^n ∧ s.IsSemiprime ∧ Odd s } - 2^n = val - 2^nn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
  have h_S : sInf { s | s > 2^n ∧ s.IsSemiprime ∧ Odd s } = val := byn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ a n = val - 2 ^ nn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
    apply IsLeast.csInf_eqn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ IsLeast {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} valn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
    constructorleftn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ val ∈ {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s}rightn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ val ∈ lowerBounds {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s}n:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
    ·leftn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ val ∈ {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s}n:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n exact ⟨h_gt, h_mem⟩All goals completed! 🐙n:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
    ·rightn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)⊢ val ∈ lowerBounds {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s}n:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n rintro x ⟨hx1, hx2⟩rightn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)x:ℕhx1:x > 2 ^ nhx2:x.IsSemiprime ∧ Odd x⊢ val ≤ xn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
      by_contra! hrightn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)x:ℕhx1:x > 2 ^ nhx2:x.IsSemiprime ∧ Odd xh:x < val⊢ Falsen:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
      exact h_min x hx1 h hx2n:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ nn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} - 2 ^ n = val - 2 ^ n
  rw [h_Sn:ℕval:ℕh_mem:val.IsSemiprime ∧ Odd valh_gt:2 ^ n < valh_min:∀ (x : ℕ), 2 ^ n < x → x < val → ¬(x.IsSemiprime ∧ Odd x)h_S:sInf {s | s > 2 ^ n ∧ s.IsSemiprime ∧ Odd s} = val⊢ val - 2 ^ n = val - 2 ^ nAll goals completed! 🐙]All goals completed! 🐙

@[category test, AMS 11]
theorem a_1 : a 1 = 7 := by⊢ a 1 = 7
  apply a_eq_of 1 9 (by⊢ IsSemiprime 9 ∧ Odd 9 native_decideAll goals completed! 🐙) (by⊢ 2 ^ 1 < 9 norm_numAll goals completed! 🐙)
  intro x h1 h2x:ℕh1:2 ^ 1 < xh2:x < 9⊢ ¬(x.IsSemiprime ∧ Odd x)
  interval_cases x«3»x:ℕh1:2 ^ 1 < 3h2:3 < 9⊢ ¬(IsSemiprime 3 ∧ Odd 3)«4»x:ℕh1:2 ^ 1 < 4h2:4 < 9⊢ ¬(IsSemiprime 4 ∧ Odd 4)«5»x:ℕh1:2 ^ 1 < 5h2:5 < 9⊢ ¬(IsSemiprime 5 ∧ Odd 5)«6»x:ℕh1:2 ^ 1 < 6h2:6 < 9⊢ ¬(IsSemiprime 6 ∧ Odd 6)«7»x:ℕh1:2 ^ 1 < 7h2:7 < 9⊢ ¬(IsSemiprime 7 ∧ Odd 7)«8»x:ℕh1:2 ^ 1 < 8h2:8 < 9⊢ ¬(IsSemiprime 8 ∧ Odd 8) <;>«3»x:ℕh1:2 ^ 1 < 3h2:3 < 9⊢ ¬(IsSemiprime 3 ∧ Odd 3)«4»x:ℕh1:2 ^ 1 < 4h2:4 < 9⊢ ¬(IsSemiprime 4 ∧ Odd 4)«5»x:ℕh1:2 ^ 1 < 5h2:5 < 9⊢ ¬(IsSemiprime 5 ∧ Odd 5)«6»x:ℕh1:2 ^ 1 < 6h2:6 < 9⊢ ¬(IsSemiprime 6 ∧ Odd 6)«7»x:ℕh1:2 ^ 1 < 7h2:7 < 9⊢ ¬(IsSemiprime 7 ∧ Odd 7)«8»x:ℕh1:2 ^ 1 < 8h2:8 < 9⊢ ¬(IsSemiprime 8 ∧ Odd 8) native_decideAll goals completed! 🐙

@[category test, AMS 11]
theorem a_2 : a 2 = 5 := by⊢ a 2 = 5
  apply a_eq_of 2 9 (by⊢ IsSemiprime 9 ∧ Odd 9 native_decideAll goals completed! 🐙) (by⊢ 2 ^ 2 < 9 norm_numAll goals completed! 🐙)
  intro x h1 h2x:ℕh1:2 ^ 2 < xh2:x < 9⊢ ¬(x.IsSemiprime ∧ Odd x)
  interval_cases x«5»x:ℕh1:2 ^ 2 < 5h2:5 < 9⊢ ¬(IsSemiprime 5 ∧ Odd 5)«6»x:ℕh1:2 ^ 2 < 6h2:6 < 9⊢ ¬(IsSemiprime 6 ∧ Odd 6)«7»x:ℕh1:2 ^ 2 < 7h2:7 < 9⊢ ¬(IsSemiprime 7 ∧ Odd 7)«8»x:ℕh1:2 ^ 2 < 8h2:8 < 9⊢ ¬(IsSemiprime 8 ∧ Odd 8) <;>«5»x:ℕh1:2 ^ 2 < 5h2:5 < 9⊢ ¬(IsSemiprime 5 ∧ Odd 5)«6»x:ℕh1:2 ^ 2 < 6h2:6 < 9⊢ ¬(IsSemiprime 6 ∧ Odd 6)«7»x:ℕh1:2 ^ 2 < 7h2:7 < 9⊢ ¬(IsSemiprime 7 ∧ Odd 7)«8»x:ℕh1:2 ^ 2 < 8h2:8 < 9⊢ ¬(IsSemiprime 8 ∧ Odd 8) native_decideAll goals completed! 🐙

@[category test, AMS 11]
theorem a_3 : a 3 = 1 := by⊢ a 3 = 1
  apply a_eq_of 3 9 (by⊢ IsSemiprime 9 ∧ Odd 9 native_decideAll goals completed! 🐙) (by⊢ 2 ^ 3 < 9 norm_numAll goals completed! 🐙)
  intro x h1 h2x:ℕh1:2 ^ 3 < xh2:x < 9⊢ ¬(x.IsSemiprime ∧ Odd x)
  interval_cases xAll goals completed! 🐙

@[category test, AMS 11]
theorem a_4 : a 4 = 5 := by⊢ a 4 = 5
  apply a_eq_of 4 21 (by⊢ IsSemiprime 21 ∧ Odd 21 native_decideAll goals completed! 🐙) (by⊢ 2 ^ 4 < 21 norm_numAll goals completed! 🐙)
  intro x h1 h2x:ℕh1:2 ^ 4 < xh2:x < 21⊢ ¬(x.IsSemiprime ∧ Odd x)
  interval_cases x«17»x:ℕh1:2 ^ 4 < 17h2:17 < 21⊢ ¬(IsSemiprime 17 ∧ Odd 17)«18»x:ℕh1:2 ^ 4 < 18h2:18 < 21⊢ ¬(IsSemiprime 18 ∧ Odd 18)«19»x:ℕh1:2 ^ 4 < 19h2:19 < 21⊢ ¬(IsSemiprime 19 ∧ Odd 19)«20»x:ℕh1:2 ^ 4 < 20h2:20 < 21⊢ ¬(IsSemiprime 20 ∧ Odd 20) <;>«17»x:ℕh1:2 ^ 4 < 17h2:17 < 21⊢ ¬(IsSemiprime 17 ∧ Odd 17)«18»x:ℕh1:2 ^ 4 < 18h2:18 < 21⊢ ¬(IsSemiprime 18 ∧ Odd 18)«19»x:ℕh1:2 ^ 4 < 19h2:19 < 21⊢ ¬(IsSemiprime 19 ∧ Odd 19)«20»x:ℕh1:2 ^ 4 < 20h2:20 < 21⊢ ¬(IsSemiprime 20 ∧ Odd 20) native_decideAll goals completed! 🐙

@[category test, AMS 11]
theorem a_5 : a 5 = 1 := by⊢ a 5 = 1
  apply a_eq_of 5 33 (by⊢ IsSemiprime 33 ∧ Odd 33 native_decideAll goals completed! 🐙) (by⊢ 2 ^ 5 < 33 norm_numAll goals completed! 🐙)
  intro x h1 h2x:ℕh1:2 ^ 5 < xh2:x < 33⊢ ¬(x.IsSemiprime ∧ Odd x)
  interval_cases xAll goals completed! 🐙

In this powers of 2 sequence, does 1 occur infinitely often?

@[category research open, AMS 11]
theorem conjecture1 :
  answer(sorry) ↔ Set.Infinite {n : ℕ | a n = 1} := by⊢ True ↔ {n | a n = 1}.Infinite
  sorryAll goals completed! 🐙

Does every odd number occur?

@[category research open, AMS 11]
theorem conjecture2 :
  answer(sorry) ↔ ∀ k : ℕ, Odd k → ∃ n : ℕ, a n = k := by⊢ True ↔ ∀ (k : ℕ), Odd k → ∃ n, OeisA114137.a n = k
  sorryAll goals completed! 🐙

end OeisA114137