Algebraic Completeness of Feynman Premeasures: The Henstock-Kurzweil Path Integral and Operator Wick Calculus in Lean 4

기술 요약: 파인만 프리메저의 대수적 완결성

문제 정의
본 연구는 위크 회전(Wick rotation, 즉 실수 시간 유지)을 사용하지 않고 무한 차원에서의 자유 장(free field)에 대한 파인만 범함수 적분을 엄밀하게 구축하는 문제를 다룬다. 주요 과제는 진동하는 커널 $e^{iS(\phi)}$의 적분을 정의하는 것인데, 이 적분은 피적분 함수의 절댓값이 항등적으로 1이므로 르베그 적분이 정의되지 않는다. 저자의 프로그램의 이전 단계에서는 특정 사례에 대해 쿨브스-스테드먼 공간(Kuelbs–Steadman spaces) 상의 헨스톡-퀴르크웰(Henstock–Kurwitz, HK) 경로 적분을 확립하였으나, 네 가지 구체적인 "미래 목표"를 미해결 상태로 남겨두었다:

1. 일관성 정리에서 "박스 분할(box divisions)"에 대한 제한을 제거하여 임의의 원통형 분할(cylindrical divisions)을 허용할 것.
2. 좌표 유도 가우시안 측도와 표준 가우시안 밀도 $\mathbb{R}^k$를 엄밀하게 식별할 것.
3. 삭스-헨스톡 보조정리(Saks–Henstock lemma), 임의의 유한 분해에 대한 가법성, 그리고 서로 다른 수의 모드($V_n$ 대 $V_m$)를 사용하는 묘사 간의 일관성을 증명할 것.
4. 위크 회전 없이 프레슬 공식(Fresnel formula)을 통해 자유 장 범함수 적분의 존재성을 확립할 것.

나아가, 본 논문은 모든 상관 함수(위크 정리) 수준에서 자유 장의 기술을 완성하고, 진동하는 프리메저를 일반적인 원통형 프리메저 이론에 삽입하고자 한다.

방법론
본 작업은 Mathlib 라이브러리 상의 Lean 4를 이용한 형식 검증 프로젝트이다. 방법론은 리만 적분을 일반화하며 절대 수렴에 실패하는 조건부 수렴 진동 적분을 처리할 수 있는 헨스톡-퀴르크웰(HK, 게이지) 적분에 의존한다.

주요 방법론적 구성 요소는 다음과 같다:

• 실린더의 기하학적 분석: 유계 박스 위의 실린더에 포함된 모든 비어 있지 않은 원통형 셀은 모든 좌표 방향을 제약함을 증명한다(정리 3.1). 이 "방향 경계(direction bound)"를 통해, 하위 박스에 정렬된 경우뿐만 아니라 임의의 원통형 분할에 대해서도 균등한 리만 합 추정이 가능하다.
• 아벨 정규화(Abelian Regularization): 위크 회전(시간을 복소 평면으로 회전시키는 것) 대신, 진동하는 커널 $e^{iax^2/2}$를 처리하기 위해 아벨 정규화 매개변수 $\varepsilon \to 0^+$를 활용한다. 이는 감쇠 매개변수의 실수 부분이 0일 때도 성립하는 균등 꼬리 추정(정리 6.1)을 증명하는 것을 포함한다.
• 스펙트럼 분해: 비대각 액션(non-diagonal actions)의 경우, 양의 정치(positive-definite) 액션 행렬 $A$의 직교 대각화를 사용하여 적분을 일차원 프레슬 적분의 곱으로 변환하며, 이때 고유 기저에 맞게 조정된 큐브를 사용한다.
• 생성 함수(Generating Functionals): 상관 함수는 유계가 아닌 다항식의 직접 적분(이는 별도의 수렴 분석을 필요로 함)이 아니라, 프레슬 공식을 통해 얻은 폐쇄형 생성 함수 $Z(j)$를 미분함으로써 도출된다.
• 형식 검증: 모든 정리는 기계적으로 검증된다. 본 형식화는 propext, Classical.choice, Quot.sound 이상의 공리를 사용하지 않으며, sorry나 admit 문을 포함하지 않는다.

주요 기여 및 결과

1. 임의의 원통형 분할 (목표 8.1):
   본 논문은 HK 적분이 하위 박스에 대한 분할 제한을 제거하고 임의의 원통형 분할에 대해 일관적임을 증명한다. "방향 경계" 정리는 게이지가 셀의 좌표를 제어하도록 보장하여, 균등한 리만 합 추정을 가능하게 한다(정리 3.3).

2. 가우시안 측도의 식별 (목표 8.2):
   $\mathbb{R}^k$ 상의 좌표 범함수에 의해 유도된 측도가 밀도 $(2\pi)^{-k/2}e^{-|y|^2/2}$를 갖는 표준 가우시안 측도와 정확히 일치함을 형식적으로 증명한다(정리 4.1).

3. 삭스-헨스톡 및 가법성 (목표 8.3):
   원통형 설정에서 삭스-헨스톡 보조정리가 확립되어, $\delta$-세밀한 부분 체계에 대한 절대 오차의 합이 유계임을 증명한다. 이는 임의의 유한 분해에 대한 적분의 가법성과, 실린더를 기술하는 데 사용된 모드의 수($n$ 대 $m$)에 관계없이 적분 값이 일치함을 이끈다(정리 5.4).

4. 프레슬 공식과 자유 장 (목표 8.4):

• 일차원 프레슬 공식: 위크 회전 없이 $\lim_{R\to\infty} \int_{-R}^R e^{iax^2/2} dx = \sqrt{2\pi/a} e^{i\pi/4}$가 부적절 게이지 적분(improper gauge integral)으로서 성립함을 증명한다(정리 6.2).
• 다차원 확장: 직교 대각화와 조정된 큐브를 사용하여 임의의 대칭 양의 정치 액션 $A$로 이를 확장한다(정리 7.2).
• 존재성: 자유 장 범함수 $e^{iS(\phi)}$는 유계 박스 위의 임의의 실린더 상에서 HK-적분 가능함이 증명된다(정리 6.5).

5. 생성 함수 및 상관 함수:

• 외부 소스를 포함한 생성 함수 $Z(j)$가 구성되며, $Z(j) = (2\pi)^{k/2} e^{i\pi k/4} (\det A)^{-1/2} \exp(-\frac{i}{2}\langle j, A^{-1}j \rangle)$의 값을 가짐을 도출한다(정리 7.3).
• 이점 함수(two-point function)는 $\langle y_p y_q \rangle = i(A^{-1})_{pq}$로 계산된다(정리 7.4).
• 위크 정리: 홀수 차수 상관 함수는 0이 되며, 짝수 차수 상관 함수는 이점 함수의 쌍(pairings)에 대한 합으로 인수분해됨을 증명한다(정리 8.6). 사점 함수(four-point function)는 특징적인 실수 시간 인자 $i$를 보여주며 명시적으로 도출된다(결론 8.7).

6. 일반 이론 및 극한:

• 진동하는 프리메저는 복소 원통형 프리메저로서 일반 이론에 삽입되며, 그 투영 일관성(projective consistency)이 증명된다(정리 9.2).
• HK 적분의 값은 프레슬 값과 동일함이 확인된다(정리 9.3).
• 감쇠된(유클리드) 가우시안 프리메저로부터 진동하는 프리메저로의 이행은 $\varepsilon \to 0^+$ 극한으로서 확립되어, 경로 회전 없이 두 그림 사이의 연결을 확인한다(정리 11.1).

7. 금융 수학에의 적용:
   기계(특히 가우시안 꼬리 항등식과 HK 일관성)의 활용 사례로서, 본 논문은 유럽형 콜 옵션의 블랙-숄즈 공식을 헨스톡-퀴르크웰 적분으로서 도출한다. 이 도출은 가우시안 원통형 프리메저에 의존하며, 위크 회전을 전혀 사용하지 않고 일차원 가우시안 꼬리 계산으로 환원된다(섹션 10).

의의 및 주장
본 논문은 헨스톡-퀴르크웰 프레임워크 내에서 자유 장에 대한 파인만 프리메저의 대수적 완결성을 달성했다고 주장한다. 구체적으로:

• 자유 장 범함수 적분이 위크 회전을 호출하지 않고도 존재하며 프레슬 값과 같음을 기계적으로 검증된 증명을 통해 제공한다.
• 단순한 이점 함수뿐만 아니라 모든 상관 함수 수준에서 위크 정리를 통해 자유 장의 기술을 완성한다.
• 진동하는 프리메저의 투영 일관성을 확립하여, 이를 일반적인 원통형 프리메저 이론 내에서 엄밀한 객체로 다룰 수 있게 한다.
• "실수 시간" 진동 적분이 아벨 정규화와 게이지 적분을 통해 엄밀하게 다뤄질 수 있음을 입증하며, 이는 유클리드(감쇠된) 접근 방식과 구별된다.

범위 및 한계
저자는 본 작업이 자유 장에 국한됨을 명시한다. 다음은 향후 연구를 위한 미해결 과제로 남아 있다:

• 상호작용하는 장(특히 무한 모드에서의 $\lambda \phi^4$).
• 유계가 아닌 생성자(Trotter–Kato 또는 $C_0$-semigroups가 필요함).
• 재규격화 및 구성적 양자장론.
• 게이지 이론의 연속체 극한(단, 이 도구는 동반 논문에서 그리보프 복사(Gribov copies)에 적용됨).

본 논문은 자신의 기여가 자유 장 사례에 대한 기계 검증된 엄밀한 종결임을 강조하며, 향후 확장을 위한 필수적인 요소들(비가우시안 영역, Chernoff–Lie–Trotter 스킴 등)을 제공하지만, 그 자체로 수행하지는 않는다는 점을 분명히 한다.