A Finite Certificate for the Positive $n=9$ Vasc Inequality

기술 요약: 양의 $n = 9$ Vasc 부등식에 대한 유한 증명서(Finite Certificate)

문제 정의
본 논문은 $n=9$인 경우의 양의 실수 Vasc 순환 부등식(Vasc cyclic inequality)에 관한 양의 실수 사례를 다룬다. Vasc 식은 $C_n(x_1, \dots, x_n) = \sum_{i=1}^n \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}}$로 정의된다(순환 인덱싱 적용). $C_n \ge 0$이라는 추측은 $n=3, 4, 5, 7$에 대해서는 증명되었으나, $n=6, 13$(그리고 결과적으로 모든 짝수 $n \ge 6$ 및 홀수 $n \ge 13$)에 대해서는 거짓임이 판명되었다. $n=9$와 $n=11$의 경우는 여전히 미해결 상태로 남아 있었다. 특히, $n=9$의 경우는 기존의 연속 차분 치환(Successive Difference Substitution, SDS) 방법이 $8! = 40,320$개의 서로 다른 정렬 영역을 분석해야 하는 조합 폭발(combinatorial explosion)에 직면하여 한계에 부딪히는 임계 지점을 나타낸다.

방법론
증명 전략은 인간이 검증 가능한 대수적 축소와 기계가 생성한 유한한 증명서(certificate)를 분리한다. 워크플로우는 다음 다섯 단계로 진행된다:

1. 분모 제거 (Denominator Clearing): 모든 분모의 양의 곱인 $D_9(x) = \prod (x_{i+1} + x_{i+2})$를 곱하여 유리 부등식을 동차 다항식 부등식 $P_9(x) \ge 0$으로 변환한다.
2. 순환 최댓값 축소 (Cyclic Maximum Reduction): 순환 불변성을 활용하여, 검증 영역을 첫 번째 좌표가 최댓값인 튜플($x_1 \ge x_i$ for all $i$)로 제한한다.
3. 정렬된 원뿔 파라미터화 (Sorted Cone Parametrization): 고정된 최댓값 원뿔 내에서, 나머지 여덟 개의 변수를 가능한 모든 순열($\sigma \in S_8$)에 따라 정렬한다. 이를 통해 $40,320$개의 "정렬된 원뿔(sorted cones)"이 생성된다.
4. 간격 좌표 변환 (Gap Coordinate Transformation): 각 정렬된 원뿔을 누적 간격 좌표($y_1, \dots, y_9$)를 사용하여 파라미터화한다. 여기서 $y_i \ge 0$은 인접한 정렬된 변수 사이의 차이를 나타낸다. 이는 문제를 양의 총 간격을 가진 비음수 직교 영역(nonnegative orthant)으로 매핑한다.
5. 유한 증명서 검증 (Finite Certificate Verification): 각 40,320개의 정렬된 원뿔에 대해 특정 "터미널 행(terminal row)"이 생성된다. 각 원뿔에서의 부등식 타당성은 다음 세 가지 건전성 메커니즘 중 하나를 검증함으로써 확립된다:
   • 계수별 비음수성 (Coefficientwise Nonnegativity): 간격 좌표에서의 다항식의 모든 계수가 비음수이다.
   • 폴리아 승수 (Polya Multiplier): 다항식에 양의 인자(폴리아 승수)를 곱하여 비음수 계수를 갖는 다항식을 얻는다.
   • AM-GM 중간점 오버레이 (AM-GM Midpoint Overlay): 산술-기하 평균(AM-GM) 회로 오버레이를 통해 다항식을 검증한다.

주요 기여 및 실행
본 연구의 주요 기여는 전체 양의 실수 공간을 포괄하는 **유한한 정확한 증명서(finite exact certificate)**를 생성하고 검증한 것이다.

• AI-인간 협업: 본 증명은 LLM 기반 에이전트인 MechMath Agent Team의 인간 유도 지원을 통해 얻어졌다. 에이전트는 증명서 검증 단계(Python 검증 프로그램 작성, 케이스 분할 생성, 터미널 분류 조직화 포함)를 자율적으로 수행했다.
• 증명서 규모: 발표된 증명서에는 36,815개의 계수 리프(coefficient leaves), 2,236개의 일반 폴리아 승수 리프, 그리고 1,269개의 AM-GM 중간점 오버레이 리프가 포함되어 있다.
• 검증 엄밀성: 저자들은 이 증명서가 단순한 계산 기록이 아니라 형식적인 산물임을 강조한다. 여기에는 저장된 데이터로부터 고정 최댓값 스트림, 다항식 해시, 잔차 체크를 직접 재계산하는 독립적인 검증기(표준 라이브러리만을 사용하는 Python으로 작성됨)가 포함되어 있어, 증명서를 생성한 코드로부터의 격리를 보장한다.

결과
본 논문은 **정리 1(Theorem 1)**을 성공적으로 증명한다: 모든 양의 실수 $x_1, \dots, x_9$에 대하여, $\sum_{i=1}^9 \frac{x_i - x_{i+1}}{x_{i+1} + x_{i+2}} \ge 0$은 성립한다.

• 이 증명은 Vasc 부등식의 상태 표(Table 1)에서 첫 번째로 열려 있던 항목을 해결한다.
• $n=11$의 경우는 여전히 미해결 상태이며, 현재는 작은 원뿔에 대한 부분적인 양의 결과만이 확보된 상태이다.

의의
본 논문은 조합적 복잡성으로 인해 차단되었던 자동 부등식 증명 분야의 오래된 미해결 문제를 해결함으로써 그 의의를 갖는다. 4만 개 이상의 영역 분석을 요구하는 문제에 대해 유한한 증명서를 생성하고 독립적으로 검증할 수 있음을 보여줌으로써, AI 에이전트가 계산적 중량(케이스 분할, 프로그램 생성, 검증)을 담당하고 인간 저자가 수학적 축소 및 검증 로직를 감사하는 하이브리드 접근 방식의 유효성을 입증한다. 본 연구는 증명서, 독립 검증기, 소스 재구축 경로를 포함한 재현 가능한 경로를 제공하여 $n=9$ Vasc 부등식에 대한 새로운 벤치마크를 설정한다.