Beatty Sequences for a Quadratic Irrational: Decidability and Applications

제시된 논문 "Beatty Sequences for a Quadratic Irrational: Decidability and Applications" (2 차 무리수에 대한 베티 수열: 결정 가능성과 응용) 은 Luke Schaeffer, Jeffrey Shallit, Stefan Zorcic 가 작성한 것으로, 2 차 무리수 (quadratic irrational) 에 기반한 비동차 베티 수열 (inhomogeneous Beatty sequence) 의 논리적 결정 가능성과 그 응용에 대한 연구입니다.

다음은 이 논문의 문제 제기, 방법론, 주요 기여, 결과 및 의의에 대한 상세한 기술적 요약입니다.

1. 문제 제기 (Problem)

• 베티 수열 (Beatty Sequence): $\alpha$가 무리수일 때, 수열 $(\lfloor n\alpha \rfloor)_{n \ge 1}$을 베티 수열이라고 합니다. 이를 일반화한 비동차 베티 수열은 $(\lfloor n\alpha + \beta \rfloor)_{n \ge 1}$ 형태를 가지며, 여기서 $\alpha, \beta$는 실수입니다.
• 연구 목표: $\alpha$와 $\beta$가 같은 2 차 수체 (quadratic field) 에 속할 때, 이 수열의 1 차 논리 (first-order logic) 이론이 **결정 가능 (decidable)**한지 여부와, 이를 통해 수열의 대수적 성질 (예: 가법 기저 여부) 을 자동으로 증명할 수 있는지에 대한 문제입니다.
• 기존 연구의 한계: 2 차 무리수에 대한 베티 수열의 결정 가능성은 Hieronymi, Terry, Baranwal 등에 의해 간접적으로 언급되거나 특정 경우 (예: 황금비) 에 대해 증명되었으나, 일반적인 2 차 무리수에 대한 간단하고 체계적인 증명 방법과 이를 활용한 구체적인 알고리즘적 응용은 부족했습니다.

2. 방법론 (Methodology)

이 논문은 자동자 (Automata) 이론과 수론을 결합한 접근법을 사용합니다.

• 오스트로프스키 표현 (Ostrowski Representation):
  • 자연수를 2 차 무리수 $\gamma$의 연분수 (continued fraction) 수렴항 (convergents) 을 기저로 하는 오스트로프스키 기수법으로 표현합니다.
  • 2 차 무리수의 경우, 이 기수법에서 덧셈 관계 ($x+y=z$) 가 유한 자동자 (finite automaton) 로 인식 가능하다는 기존 결과를 활용합니다.
• 동기화된 수열 (Synchronized Sequences):
  • 수열 $(s_n)$이 **동기화 (synchronized)**되었다는 것은, 입력 $n$과 출력 $y$의 오스트로프스키 표현을 병렬로 받아 $y = s_n$인지 판별하는 유한 자동자가 존재함을 의미합니다.
  • 저자는 $\alpha, \beta \in \mathbb{Q}(\gamma)$일 때, $n \mapsto \lfloor n\alpha + \beta \rfloor$가 $\gamma$-오스트로프스키 동기화 수열임을 증명합니다.
• Walnut 소프트웨어 활용:
  • 결정 절차 (decision procedure) 를 구현한 오픈 소스 소프트웨어 Walnut을 사용합니다.
  • Walnut 은 1 차 논리 명제를 입력받아 자동자를 생성하거나 참/거짓을 판별할 수 있습니다. 이를 통해 복잡한 수학적 명제를 기계적으로 증명합니다.

3. 주요 기여 및 결과 (Key Contributions and Results)

A. 주요 정리 (Main Theorems)

• 정리 9 (Theorem 9): $0 < \gamma < 1$이 2 차 무리수이고 $1/\gamma$의 연분수가 순수 주기적 (purely periodic) 이며, $\alpha, \beta$가 $\mathbb{Q}(\gamma)$에 속할 때, 비동차 베티 수열 $(\lfloor n\alpha + \beta \rfloor)_{n \ge 1}$은 $\gamma$-오스트로프스키 동기화 수열입니다.
  • 이는 $\alpha, \beta$가 2 차 무리수 $\gamma$와 같은 수체에 속하는 한, 해당 수열이 자동자 이론으로 다룰 수 있음을 의미합니다.
• 정리 11 (Corollary 11): 위 조건 하에서, 자연수 집합에 덧셈과 함수 $n \mapsto \lfloor n\alpha + \beta \rfloor$를 포함하는 1 차 논리 이론은 **결정 가능 (decidable)**합니다.
  • 즉, 해당 수열에 대한 1 차 논리 명제 (예: "모든 충분히 큰 정수는 이 수열의 원소들의 합으로 표현 가능한가?") 는 알고리즘적으로 참/거짓을 판별할 수 있습니다.
• 역정리 (Theorem 28): 만약 베티 수열이 $\gamma$-동기화된다면, $\alpha$와 $\beta$는 반드시 $\mathbb{Q}(\gamma)$에 속해야 합니다. 이는 동기화 가능성과 2 차 수체 소속성 사이의 필요충분 조건을 보여줍니다.

B. 응용 분야 및 구체적 문제 해결

이론적 결과를 바탕으로 Walnut 을 사용하여 다음과 같은 문제들을 해결했습니다:

1. 가법 기저 (Additive Basis) 판별:
   • 주어진 $r \ge 1$에 대해, 베티 수열의 원소들이 $r$개의 합으로 모든 자연수 (또는 충분히 큰 자연수) 를 표현할 수 있는지 (가법 기저 또는 점근적 가법 기저 여부) 를 결정할 수 있음을 보였습니다.
2. Don Reble 의 추측 증명:
   • OEIS 시퀀스 A189377, A189378, A189379 와 관련된 Reble 의 추측 (피보나치 단어 내의 단색 산술 진행에 관한 것) 을 Walnut 을 통해 1 초 미만으로 증명했습니다.
3. Graham 의 질문 해결:
   • 서로 다른 2 차 무리수 쌍들의 집합이 "최종 덮개 가족 (eventual covering family)"이 되는지 여부를 결정 가능함을 보였습니다.
4. Hildebrand et al. 의 수열 분석:
   • Hildebrand 등이 연구한 수열 $\tilde{c}(n)$에 대해, $0 \le c(n) - \tilde{c}(n) \le 2$라는 부등식을 증명하고 명시적인 자동자를 구성했습니다.
5. Kimberling 의 Swappage 문제:
   • Kimberling 이 제안한 "lower even swappage sequence" 등 여러 OEIS 시퀀스에 대한 추측을 증명하고, 이를 간단한 폐쇄형 식으로 표현했습니다.
6. $\sqrt{2}$ 관련 수열:
   • $\sqrt{2}$와 관련된 7 개의 OEIS 시퀀스 (A097508 등) 에 대한 오스트로프스키 자동자를 구성하고, Michel Dekking 등의 추측을 증명했습니다.
7. 분수부 (Fractional Parts) 비교:
   • $\{ \alpha x + \beta \} < \{ \alpha' y + \beta' \}$와 같은 분수부 비교 명제도 Walnut 에서 처리 가능함을 보였습니다.

4. 의의 및 의의 (Significance)

• 간단한 증명 방법론: 기존에 복잡하거나 간접적이었던 2 차 무리수 베티 수열의 결정 가능성에 대한 증명을, 동기화된 수열 (synchronized sequences) 개념을 통해 매우 간결하고 구조적으로 재구성했습니다.
• 실용적인 자동화: Walnut 을 통해 이론적 결정 가능성뿐만 아니라, 구체적인 수열에 대한 정리들을 자동으로 증명할 수 있음을 보여주었습니다. 이는 수론과 조합론의 많은 미해결 문제를 기계적으로 접근할 수 있는 새로운 길을 열었습니다.
• 역사적 문제 해결: Reble, Kimberling, Graham 등 수학자들이 제기한 구체적인 오픈 문제들을 해결함으로써, 자동자 이론이 순수 수학의 난제를 푸는 강력한 도구가 될 수 있음을 입증했습니다.
• 일반성: 이 방법은 황금비뿐만 아니라 임의의 2 차 무리수 (예: $\sqrt{2}, \sqrt{7}$ 등) 에 대해 적용 가능하여, 베티 수열 연구의 범위를 크게 확장했습니다.

결론

이 논문은 2 차 무리수 기반의 비동차 베티 수열이 오스트로프스키 표현 하에서 동기화됨을 증명함으로써, 해당 수열의 1 차 논리 이론이 결정 가능함을 확립했습니다. 이를 바탕으로 개발된 Walnut을 활용한 알고리즘은 복잡한 수학적 추측을 기계적으로 검증하고, 가법 기저 성질, 분수부 비교, 다양한 OEIS 시퀀스의 성질을 규명하는 데 성공했습니다. 이는 자동자 이론과 수론의 융합 연구에서 중요한 이정표가 되는 작업입니다.