FormalConjectures.OEIS.«108864»

/-
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.
-/
module

public import FormalConjecturesUtil

Numbers $n$ such that the perfect deficiency of $n$ is $\le 10$.

The perfect deficiency of $n$ (A109883) is the remainder after greedily subtracting from $n$ its divisors in increasing order, skipping any divisor larger than the current remainder.

References:

A108864

A109883

@[expose] public sectionnamespace OeisA108864open Nat Finset Int

The perfect deficiency of $n$ (A109883): the remainder after greedily subtracting from $n$ its divisors in increasing order, skipping any divisor larger than the current remainder.

def perfectDeficiency (n : ℕ) : ℕ :=
  (List.range (n + 1)).foldl (fun m d => if d ∣ n ∧ d ≤ m then m - d else m) n

The condition for a number $n$ to be in the sequence. It satisfies $0 < n$ and its perfect deficiency is $\le 10$.

def A (n : ℕ) : Prop :=
  0 < n ∧ perfectDeficiency n ≤ 10

instance : DecidablePred A := by⊢ DecidablePred A
  unfold A⊢ DecidablePred fun n ↦ 0 < n ∧ perfectDeficiency n ≤ 10
  infer_instanceAll goals completed! 🐙

The primary defining sequence a. $a(n)$ is the $n$-th number (0-indexed) such that its perfect deficiency is $\le 10$.

noncomputable def a (n : ℕ) : ℕ :=
  n.nth A

Term theorems verifying the first few values of the sequence against the official OEIS b-file


@[category test, AMS 11]
theorem a_0 : a 0 = 1 := by⊢ a 0 = 1
  have h1 : A 1 := by decideh1:A 1⊢ a 0 = 1h1:A 1⊢ a 0 = 1
  have hcnt : Nat.count A 1 = 0 := by decideh1:A 1hcnt:count A 1 = 0⊢ a 0 = 1h1:A 1hcnt:count A 1 = 0⊢ a 0 = 1
  have := Nat.nth_count (p := A) h1h1:A 1hcnt:count A 1 = 0this:nth A (count A 1) = 1⊢ a 0 = 1
  rwa [hcnth1:A 1hcnt:count A 1 = 0this:nth A 0 = 1⊢ a 0 = 1]h1:A 1hcnt:count A 1 = 0this:nth A 0 = 1⊢ a 0 = 1 at this



@[category test, AMS 11]
theorem a_1 : a 1 = 2 := by⊢ a 1 = 2
  have h2 : A 2 := by decideh2:A 2⊢ a 1 = 2h2:A 2⊢ a 1 = 2
  have hcnt : Nat.count A 2 = 1 := by decideh2:A 2hcnt:count A 2 = 1⊢ a 1 = 2h2:A 2hcnt:count A 2 = 1⊢ a 1 = 2
  have := Nat.nth_count (p := A) h2h2:A 2hcnt:count A 2 = 1this:nth A (count A 2) = 2⊢ a 1 = 2
  rwa [hcnth2:A 2hcnt:count A 2 = 1this:nth A 1 = 2⊢ a 1 = 2]h2:A 2hcnt:count A 2 = 1this:nth A 1 = 2⊢ a 1 = 2 at this



@[category test, AMS 11]
theorem a_2 : a 2 = 3 := by⊢ a 2 = 3
  have h3 : A 3 := by decideh3:A 3⊢ a 2 = 3h3:A 3⊢ a 2 = 3
  have hcnt : Nat.count A 3 = 2 := by decideh3:A 3hcnt:count A 3 = 2⊢ a 2 = 3h3:A 3hcnt:count A 3 = 2⊢ a 2 = 3
  have := Nat.nth_count (p := A) h3h3:A 3hcnt:count A 3 = 2this:nth A (count A 3) = 3⊢ a 2 = 3
  rwa [hcnth3:A 3hcnt:count A 3 = 2this:nth A 2 = 3⊢ a 2 = 3]h3:A 3hcnt:count A 3 = 2this:nth A 2 = 3⊢ a 2 = 3 at this



@[category test, AMS 11]
theorem a_3 : a 3 = 4 := by⊢ a 3 = 4
  have h4 : A 4 := by decideh4:A 4⊢ a 3 = 4h4:A 4⊢ a 3 = 4
  have hcnt : Nat.count A 4 = 3 := by decideh4:A 4hcnt:count A 4 = 3⊢ a 3 = 4h4:A 4hcnt:count A 4 = 3⊢ a 3 = 4
  have := Nat.nth_count (p := A) h4h4:A 4hcnt:count A 4 = 3this:nth A (count A 4) = 4⊢ a 3 = 4
  rwa [hcnth4:A 4hcnt:count A 4 = 3this:nth A 3 = 4⊢ a 3 = 4]h4:A 4hcnt:count A 4 = 3this:nth A 3 = 4⊢ a 3 = 4 at this



@[category test, AMS 11]
theorem a_4 : a 4 = 5 := by⊢ a 4 = 5
  have h5 : A 5 := by decideh5:A 5⊢ a 4 = 5h5:A 5⊢ a 4 = 5
  have hcnt : Nat.count A 5 = 4 := by decideh5:A 5hcnt:count A 5 = 4⊢ a 4 = 5h5:A 5hcnt:count A 5 = 4⊢ a 4 = 5
  have := Nat.nth_count (p := A) h5h5:A 5hcnt:count A 5 = 4this:nth A (count A 5) = 5⊢ a 4 = 5
  rwa [hcnth5:A 5hcnt:count A 5 = 4this:nth A 4 = 5⊢ a 4 = 5]h5:A 5hcnt:count A 5 = 4this:nth A 4 = 5⊢ a 4 = 5 at this

Is $1155$ the last odd number in this sequence? ($1155$ is the $59$th term starting from $1$, corresponding to $a(58) = 1155$).

@[category research open, AMS 11]
theorem conjecture :
    answer(sorry) ↔ ∀ n > 58, Even (a n) := by⊢ True ↔ ∀ n > 58, Even (OeisA108864.a n)
  sorryAll goals completed! 🐙

end OeisA108864