Proving Properties of $φ$-Representations with the Walnut Theorem-Prover

이 논문은 Walnut 정리 증명기를 활용하여 Frougny 와 Sakarovitch 의 고전 정리를 새로운 계산적 방식으로 재증명하고, 이를 통해 $\phi$-표현에 관한 기존 및 새로운 결과들을 통일적이고 자동화된 방식으로 유도함을 보여줍니다.

핵심

🌟 1. 황금비 (φ) 라는 새로운 언어

우리는 보통 10 진법 (0~9) 이나 2 진법 (0 과 1) 으로 숫자를 표현합니다. 하지만 이 논문은 **'φ (파이, 약 1.618)'**라는 특별한 숫자를 '기저 (base)'로 사용하는 새로운 언어를 다룹니다.

• 비유: 마치 우리가 "10"이라고 말할 때 "10 개의 1"을 의미하듯, φ-표현법에서는 "1"이 "약 1.618"을 의미합니다.
• 문제: 이 φ-언어로 숫자를 쓸 때, 규칙이 까다롭습니다. 예를 들어, "11"이라는 연속된 숫자는 쓸 수 없거나, 특정 위치에만 쓸 수 있습니다. 이 규칙을 지키는 '표준형 (Canonical)' 숫자를 찾는 것은 매우 어렵고 지루한 작업입니다.

🤖 2. 월넛 (Walnut): 수학적 문제를 해결하는 '자동 번역기'

저자는 이 복잡한 규칙을 사람이 일일이 손으로 증명하는 대신, **'월넛'**이라는 소프트웨어를 사용했습니다.

• 월넛이 뭐죠? 수학의 논리 문장을 입력하면, "이 말이 맞나요?"라고 물어보는 자동화 도구입니다. 마치 "이 문장이 문법적으로 맞나요?"를 체크하는 스펠링 체커처럼, "이 숫자 표현이 φ-규칙을 따르나요?"를 자동으로 확인해 줍니다.
• 작동 원리: 월넛은 논리를 입력하면, 그 규칙을 따르는 모든 숫자를 찾아내는 **'자동 기계 (오토마타)'**를 만들어냅니다. 이 기계는 숫자를 입력하면 "네, 맞습니다" 또는 "아니요, 틀렸습니다"라고 딱딱하게 판단합니다.

🔍 3. 이 논문이 해낸 일: "복잡한 증명, 이제 자동화!"

이 논문은 과거의 수학자들이 수년 동안 손으로 증명해야 했던 어려운 문제들을 월넛을 통해 순식간에 해결했습니다.

A. '접힌' 지도를 펴기 (Folded Representation)

φ-표현법은 소수점 앞 (정수부) 과 뒤 (소수부) 가 뒤섞여 있는 것처럼 복잡합니다.

• 비유: 마치 접힌 우편물을 펴서 읽는 것처럼, 월넛은 정수부와 소수부를 동시에 읽어서 "이 숫자가 맞는지" 확인하는 3 입력 기계를 만들었습니다.
• 결과: 이 기계를 통해 피보나치 수 (1, 1, 2, 3, 5...) 나 루카스 수 (2, 1, 3, 4, 7...) 같은 특별한 숫자들이 φ-언어로 어떻게 쓰이는지 그 패턴을 완벽하게 찾아냈습니다.

B. 거울 속의 숫자 (팰린드롬)

"121"처럼 앞뒤가 같은 숫자를 '팰린드롬'이라고 합니다.

• 질문: φ-언어로 표현했을 때, 앞뒤가 같은 숫자는 어떤 것들이 있을까요?
• 해결: 월넛은 이 조건을 만족하는 모든 숫자를 찾아내는 기계를 만들었습니다. "2, 14, 36..." 같은 숫자들이 그 목록에 있다는 것을 증명했습니다.

C. 숫자 세기 (Knott Expansion)

어떤 숫자를 φ-언어로 표현할 때, 규칙을 약간만 바꾸면 (예: "11"을 허용하되 특정 조건만 붙이면) 같은 숫자를 표현하는 방법이 여러 가지가 생길 수 있습니다.

• 과거: 수학자들은 "이 숫자는 표현법이 3 가지, 저 숫자는 5 가지"라고 하나하나 세거나 복잡한 수학적 귀납법으로 증명해야 했습니다.
• 현재: 월넛은 "표현법이 가능한 경우의 수를 자동으로 계산하는 기계"를 만들어, 어떤 숫자가 나오든 순식간에 답을 알려줍니다.

🎨 4. 왜 이것이 중요한가요?

이 논문의 핵심 메시지는 **"수학의 아름다움은 복잡한 증명에 있는 것이 아니라, 규칙을 발견하고 자동화하는 데 있다"**는 것입니다.

• 과거: 수학자들은 복잡한 논리 (귀납법) 를 써서 "이건 맞고 저건 틀려"라고 싸웠습니다.
• 현재: 월넛이라는 도구를 통해 "이 규칙을 입력하면 컴퓨터가 모든 경우를 확인하고 답을 줍니다"라고 말합니다.
• 효과: 이전에는 100 페이지 분량의 논문으로 증명해야 했던 내용도, 이제는 몇 줄의 코드와 자동 기계로 증명할 수 있게 되었습니다. 이는 수학 연구의 방식을 완전히 바꾼 혁신입니다.

💡 요약

이 논문은 **"황금비 (φ) 라는 낯선 언어로 숫자를 쓰는 규칙"**을 **월넛 (Walnut)**이라는 자동 번역기를 이용해 분석한 이야기입니다.

• 과거의 방식: 손으로 하나하나 증명하는 고된 노동.
• 이 논문의 방식: 규칙을 컴퓨터에 입력하면, 컴퓨터가 모든 숫자를 검사하고 새로운 패턴을 찾아내는 자동화.

저자는 이 방법을 통해 기존에 알려진 많은 수학 정리를 더 쉽고 빠르게 증명했을 뿐만 아니라, 아예 새로운 숫자 패턴들도 발견해냈습니다. 마치 복잡한 퍼즐을 사람이 직접 맞추는 대신, 퍼즐을 맞춰주는 로봇을 만들어 모든 조각을 순식간에 맞춰놓은 것과 같습니다.

이 연구는 수학이 더 이상 '고독한 천재의 작업'이 아니라, 컴퓨터와 협력하여 새로운 지식을 발견하는 시대로 나아가고 있음을 보여줍니다.

기술 요약

1. 연구 배경 및 문제 제기 (Problem)

• φ-표현 (φ-representation): 1957 년 George Bergman 은 임의의 음이 아닌 실수 $z$를 황금비 $\phi = (1+\sqrt{5})/2$를 기저로 하는 표현으로 전개할 수 있음을 보였습니다. 즉, $z = \sum a_i \phi^i$ ($a_i \in \{0, 1\}$) 형태입니다. 이 표현에서 인접한 두 자릿수가 모두 1 이 되지 않도록 ($a_i a_{i+1} \neq 1$) 제한하면 '정규 (canonical)' 표현이 유일하게 결정됩니다.
• 기존 연구의 한계: Frougny 와 Sakarovitch 는 정수의 정규 φ-표현을 계산하는 유한 오토마타 (Finite Automaton) 가 존재함을 증명했습니다. 그러나 그들의 논문은 오토마타의 구성이 매우 복잡하고 직접적으로 제시되지 않아, 이를 활용하여 새로운 성질을 증명하거나 기존 결과를 재검증하는 것이 어려웠습니다.
• 주요 문제: φ-표현과 관련된 다양한 성질 (자릿수 합, 길이의 변화, 회문 (palindrome) 성질, Knott 확장 등) 을 증명하고 새로운 결과를 도출하기 위해, Frougny-Sakarovitch 오토마타를 명시적으로 구성하고 이를 자동화하여 적용할 수 있는 체계적인 방법이 필요했습니다.

2. 방법론 (Methodology)

이 논문은 Walnut이라는 자동 정리 증명기 (Theorem-Prover) 를 핵심 도구로 사용합니다. Walnut 은 Presburger 산술의 확장판에 대한 결정 절차 (decision procedure) 를 사용하여 자동 시퀀스 (automatic sequences) 와 관련된 정리를 증명하거나 반증할 수 있습니다.

• 오토마타 구성 전략:
  1. 입력 표현: 정수 $n$을 Zeckendorf 표현 (피보나치 수열 기반) 과 NegaFibonacci 표현 (음수 피보나치 수열 기반) 으로 변환합니다.
  2. 오토마타 모듈화: Frougny-Sakarovitch 오토마타를 구성하기 위해 다음과 같은 하위 모듈들을 Walnut 코드로 정의합니다.
     • fibnorm, negfibnorm: 임의의 이진 문자열을 정규 Zeckendorf/NegaFibonacci 표현으로 변환/검증.
     • shiftl, shiftr: 비트 시프트 연산.
     • lstbit: 문자열의 끝 비트 추출.
     • fibnegfib: NegaFibonacci 표현과 Zeckendorf 표현 간의 변환.
  3. 논리적 공식화: φ-표현의 좌변 (정수부) 과 우변 (소수부) 을 $\phi$와 1 의 선형 결합 ($c\phi + d$) 으로 표현하고, 이를 통해 $n = [x.y]_\phi$가 성립하는 조건을 1 차 논리 (First-order logic) 공식으로 변환합니다.
  4. 자동화 증명: Walnut 은 이러한 논리식을 입력받아 해당 조건을 만족하는 입력값을 받아들이는 유한 오토마타를 자동으로 생성합니다. 생성된 오토마타를 통해 특정 성질이 참인지 확인하거나, 선형 표현 (linear representation) 을 유도하여 수열의 성질을 분석합니다.

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

이 논문은 Walnut 을 사용하여 기존 결과를 간결하게 재증명하고, 여러 새로운 결과를 도출했습니다.

A. Frougny-Sakarovitch 오토마타의 명시적 구성

• 논문의 핵심 목표인 Frougny-Sakarovitch 오토마타를 Walnut 코드를 통해 명시적으로 구성했습니다.
• 이 오토마타는 $n$ (Zeckendorf), $x$ (φ-표현 좌변), $y$ (φ-표현 우변의 역순) 를 병렬로 입력받아 $n = [x.y]_\phi$인지 판단합니다.
• 이를 통해 정규 φ-표현을 가진 피보나치 수 ($F_n$) 와 루카스 수 ($L_n$) 의 패턴을 자동으로 증명했습니다 (예: $F_{4i}$의 φ-표현 패턴 등).

B. φ-표현의 다양한 성질 증명

1. 자릿수 합 (Sum of digits):
   • Zeckendorf 표현의 자릿수 합이 φ-표현의 자릿수 합보다 작거나 같다는 Dale Gerdemann 의 2012 년 추측을 증명했습니다 (Theorem 3.1).
   • 이를 위해 오토마타의 전이 그래프에 가중치를 부여하고 Bellman-Ford 알고리즘을 사용하여 경로 가중치의 합이 항상 음수가 아님을 검증했습니다.
2. 표현의 길이 (Length):
   • φ-표현의 좌변 길이의 증가 패턴을 분석하고, 길이가 1 증가하는 조건이 루카스 수와 관련됨을 증명했습니다.
3. 개별 비트 (Individual bits):
   • φ-표현의 특정 위치 비트 ($d_0(n), d_1(n), d_{-1}(n)$) 가 Sturmian 시퀀스나 Lucas 수의 표현과 어떻게 연결되는지 characterization 했습니다. 특히 $d_{-1}(n)=1$인 경우와 Lucas 수의 두 가지 다른 표현이 존재하는 경우의 동치 관계를 증명했습니다.
4. 회문 및 반회문 (Palindromic & Anti-palindromic):
   • 정규 및 비정규 φ-표현이 회문 (palindrome) 이나 반회문 (antipalindrome) 인 정수 $n$을 식별하는 오토마타를 구성하고, 해당 수열을 OEIS 에 등록했습니다.

C. 새로운 확장 (Expansions) 연구

• Knott 확장: 011 로 끝나지 않는 φ-표현. Dekking 과 Van Loon 의 복잡한 유도 과정을 Walnut 을 통해 자동화하여 총 개수를 계산하는 선형 표현을 얻었고, 피보나치/루카스 수에 대한 닫힌 형식 (closed form) 을 유도했습니다.
• Natural 및 DVL 확장: Dekking 과 Van Loon 이 제안한 다른 형태의 확장 (Natural expansion, DVL-expansion) 에 대해 오토마타를 구성하고 기존 논문의 결과를 자동적으로 재증명했습니다.

D. 대수적 정수 (Algebraic Integers)

• $\mathbb{Q}(\sqrt{5})$의 대수적 정수 ($m\phi + n$) 에 대한 φ-표현을 계산하는 오토마타를 구성하여, 좌변과 우변의 길이가 같은 경우를 판별하는 방법을 제시했습니다.

4. 의의 및 중요성 (Significance)

1. 계산적 직접성 (Computational Directness): 기존에 복잡한 수학적 유도나 귀납법 (induction) 을 필요로 했던 증명들을 Walnut 을 통해 "자동적 (automatic)"이고 "직관적"인 방식으로 대체했습니다. 이는 증명 과정을 단순화하고 오류 가능성을 줄였습니다.
2. 일반화 가능성: 이 방법론은 $\phi$뿐만 아니라 2 차 Pisot 수 (quadratic Pisot numbers) $\beta$를 기저로 하는 $\beta$-확장에 대해서도 적용 가능함을 시사합니다. Walnut 이 피보나치 및 NegaFibonacci 수열을 이미 구현하고 있어, $\phi$에 대한 적용이 특히 용이했습니다.
3. 새로운 발견: 자동화된 오토마타 생성을 통해 기존 문헌에서 다루지 않았던 새로운 수열 (OEIS 등재) 과 성질들을 발견할 수 있었습니다.
4. 도구의 활용: Walnut 이 단순한 계산 도구를 넘어, 수론과 오토마타 이론의 교차 영역에서 강력한 증명 도구로 활용될 수 있음을 보여주었습니다.

결론

이 논문은 Walnut 정리 증명기를 활용하여 φ-표현 (Base-φ representation) 의 구조적 성질을 체계적으로 분석하고 증명하는 새로운 패러다임을 제시했습니다. 복잡한 수학적 증명을 자동화함으로써 기존 결과를 간결하게 재증명했을 뿐만 아니라, Knott 확장, 회문 성질, 대수적 정수 표현 등 다양한 분야에서 새로운 결과를 도출하는 데 성공했습니다. 이는 자동 시퀀스 이론과 수론의 결합을 통한 계산적 수학 연구의 모범 사례로 평가됩니다.