A Lean-Certified Proof of $K_8(4, 2) = 23$

기술 요약: $K_8(4,2) = 23$에 대한 Lean 인증 증명

문제 정의
본 논문은 $q$-진 Hamming 공간의 길이 $n$, 반경 $r$인 커버링 코드의 최소 크기인 $K_q(n,r)$의 정확한 값을 결정하는 문제를 다룹다. 구체적으로, 본 연구는 팔진수(octonary) 사례인 길이 4, 반경 2인 경우 $K_8(4,2)$의 값을 해결한다. 이 연구 이전에는 기존의 Kéri 테이블에 의해 이 값이 $[22, 23]$ 구간에 위치하는 것으로 알려져 있었다. 하한값은 Rodemich rook-domain bound를 통해 도출되었고, 상한값은 대규모 알파벳(large-alphabet) bound에 의해 뒷받침되었다. 본 연구의 목표는 $K_8(4,2) \ge 23$임을 증명하여 이 구간을 닫는 것이다.

방법론
증명은 mathlib 라이브러리를 사용하는 Lean 4 정리 증명기(theorem prover) 내에서 정형화되었다. 본 연구는 명시적인 상한(upper bound)과 구조적 하한(lower bound)이라는 두 가지 독립적인 인증서를 통해 결과를 확립하는 "증명 전달(proof-carrying)" 접근 방식을 채택한다.

1. 상한 ($K_8(4,2) \le 23$):
   저자들은 $(\text{Fin } 8)^4$ 내의 23개 코드워드로 구성된 명시적인 코드를 제공한다. 정형 증명은 두 가지 조건을 검증한다: 집합의 카디널리티가 최대 23이고, 주변 공간(4096개의 단어)의 모든 단어가 적어도 하나의 코드워드와 Hamming 거리 2 이내에 있다는 것이다. 이는 전수 조사(exhaustive finite check)이다.

2. 하한 ($K_8(4,2) \ge 23$):
   본 논문의 핵심은 크기가 22 이하인 임의의 가설적 커버 $C^*$에 대한 구조적 부존재 논증이다. 증명은 다음과 같은 일련의 축소 과정을 거친다:

   • 파이버 카운팅 (Fiber Counting): 가설적 커버를 위해, 저자들은 "파이버(fibers)" $C^*_{i,a}$ (좌표 $i$에서 심볼 $a$를 갖는 코드워드들)를 정의한다. 그들은 모든 파이버가 적어도 두 개의 코드워드를 포함해야 함을 증명한다. 이는 좌표당 16개($8 \text{ symbols} \times 2$)의 코드워드라는 기준선을 설정하며, $|C^*|=22$인 경우 최대 6개의 여분(excess) 코드워드(또는 $|C^*| \le 21$인 경우 5개)를 남긴다.
   • 누락된 쌍 그래프 (Missing-Pair Graphs): 증명은 코드의 좌표 쌍에 대한 투영(projection)에서 어떤 심볼 쌍이 누락되었는지 분석하는 "역(inverse)" 관점으로 전환한다. 이 누락된 쌍들은 그래프 $E_{ij}$를 형성한다.
   • Case $|C^*| \le 21$: 적은 여분 예산을 사용하여, 저자들은 조합론적 카운팅을 통해 누락된 쌍 그래프가 "동시 4-분할 클리크(simultaneous four-partite clique)"(여섯 개의 좌표 쌍 모두가 누락된 네 개의 심볼 $a,b,c,d$의 집합)를 포함해야 함을 보여준다. 보조정리 7은 이러한 클리크가 유효한 반경-2 커버 내에서 존재할 수 없음을 증명하며, 따라서 21 이하의 크기를 갖는 커버를 배제한다.
   • Case $|C^*| = 22$: 남은 경우에 대해, 증명은 누락된 쌍 그래프의 "프로파일(profile)"을 유한하게 분류하는 문제로 축소된다. 저자들은 유효한 프로파일이라면 반드시 특정 "공통 $3+3+2$ 블록 구조(common $3+3+2$ block structure)"를 보여야 함을 입증한다.
   • SAT/LRAT 통합: 이러한 프로파일의 분류는 수동 열거를 하기에는 너무 크다. 저자들은 제약 조건(행/열 차수 상한 및 클리크 부재 조건)을 논리곱 표준형(CNF) 인스턴스로 인코딩한다. 그들은 신뢰할 수 없는 SAT 솔버를 사용하여 불만족 증명(unsatisfiability)인 선형 RAT(LRAT) 반박(refutation)을 생성한다.
   • 정형 검증: Lean은 이 LRAT 인증서를 파싱하고, 솔버의 반박을 기계적으로 재현하여 코드의 크기가 22인 커버가 존재하지 않음을 증명한다.
   • 최종 모순: 공통 블록 구조가 가정되더라도, 저자들은 해당 구조의 "2-심볼 컴포넌트(2-symbol component)"에서 모순을 도출한다. 이 컴포넌트는 최대 4개의 행을 가진 길이 4의 이진 강도-2 배열(binary strength-2 array)을 요구하는데, 이는 수학적으로 불가능하다.

주요 기여

• 정확한 값: 본 논문은 $K_8(4,2) = 23$이라는 정확한 값을 확립하여, 기존의 $[22, 23]$ 구간을 닫는다.
• 정형화된 하한: 파이버 카운트와 누락된 쌍 그래프로부터 도출된 구조적 장애물을 통해 22-단어 커버를 모두 배제하는 완전하게 정형화된 Lean 4 증명을 제공한다. 이는 단순한 부피(volume) 논증이 아니라 구조적 장애물을 통한 것이다.
• 증명 전달 아티팩트: 결과는 명시적 코드, 구조적 보조정리, CNF 인스턴스, 그리고 LRAT 반박을 포함하는 Lean 아티팩트로 패키징된다. 결정적으로, SAT 솔버는 신뢰할 수 있는 컴퓨팅 기반(trusted computing base)의 일부가 아니며, Lean은 내부적으로 LRAT 인증서를 검증한다.
• 컴퓨팅 하한을 위한 패턴: 본 논문은 솔버가 생성한 증거를 커버링 코드 하한에 결합하는 재사용 가능한 패턴을 제시한다. 이는 "발견"(신뢰할 수 없는 솔버)과 "검증"(신뢰할 수 있는 Lean 커널)을 분리하여, 대규모 유한 분류 문제를 정식으로 검증하면서도 계산적으로 해결할 수 있게 한다.

결과
주요 결과는 정리 $K_8(4,2) = 23$이다.

• 상한: 23-단어 코드를 통해 증명됨.
• 하한: 22-단어 커버가 불가능한 이진 배열을 함의하는 "공통 $3+3+2$ 블록 시스템"을 강제한다는 모순을 보여줌으로써 증명됨.
• 성능: 정형 검증에는 상당한 계산 자원이 소요된다. 메인 증명 파일의 커널 모드 재현에는 약 143 GiB의 RAM이 필요했으나, 네이티브 모드에서는 이를 약 5.5 GiB로 줄였다. LRAT 체크 단계는 커널 모드에서 약 17분이 소요되었다.

의의 및 주장
본 논문은 주로 정형 수학과 조합론적 추론을 계산적 인증서와 결합하는 방법론의 영역에서 의의를 갖는다.

• 방법론적 전환: 구조적 조합론이 "증명 전달" 방식의 계산적 증거와 결합될 수 있음을 보여준다. SAT 솔버는 유한한 장애물을 발견하는 데 사용되지만, 수학적 가교와 솔버 출력의 검증은 전적으로 정리 증명기 내에서 처리된다.
• 신뢰 경계: SAT 솔버가 포함된 정형 증명에서의 신뢰 경계를 명확히 한다. 솔버는 신뢰할 수 없으며, Lean 커널은 LRAT 인증서와 이 인증서들을 커버링 코드 문장으로 연결하는 논리적 연역을 검사한다.
• 확장성: 본 연구는 수동 증명에는 너무 크지만 SAT 솔버로 해결 가능한 유한 분류 문제로 축소될 수 있는 커버링 코드 문제를 다루는 테스트 케이스 역할을 한다.
• 새로운 응용 없음: 본 논문은 $K_8(4,2)=23$이라는 값 자체에 대한 새로운 응용을 주장하거나 새로운 실험적 프로토콜을 제안하지 않는다. 본 논문의 기여는 순수하게 코딩 이론 테이블의 특정 미해결 문제를 해결하고, 이러한 문제들을 위한 정형 검증 워크플로우를 시연하는 데 있다.