The continuous functional calculus in Lean

기술 요약: Lean에서의 연속 함수 계산(The Continuous Functional Calculus)

문제 제기
연속 함수 계산은 $C^*$-대수 이론의 기초적인 도구로, 가환 $C^*$-부분대수를 컴팩트 하우스도르프 공간 위의 연속 함수 대수와 동일시할 수 있게 해준다. 수학적으로는 매우 잘 알려져 있지만, 이를 Lean과 같은 증명 보조기(proof assistant)에서 형식화하는 것은 상당한 어려움을 수반한다. 주요 난점은 수학적 충실도와 사용성(usability) 사이의 균형을 맞추는 데 있다. "자연스러운" 수학적 정의는 종종 의존 타입(dependent types, 예: 특정 원소의 스펙트럼에 대해서만 정의된 함수)이나 번들 구조(bundled structures, 예: 특정 타입으로서의 연속 사상)에 의존한다. 이러한 방식은 엄밀하기는 하지만, 형식적 증명 과정에서 마찰을 일으킨다. 예를 들어, 타입이 특정 원소에 의존하게 되면 등식의 재작성(rewriting)이 어려워지며, 함수의 합성(composition)을 위해서는 복잡한 서브타입 코어션(subtype coercion)과 연속성 증명을 관리해야 한다. 저자들은 엄격한 수학적 단순성을 우선시하는 설계가 Mathlib과 같은 라이브러리에 요구되는 실질적인 사용성 "리트머스 테스트"를 통과하지 못한다는 점을 확인하였다.

방법론 및 설계 결정
저자들은 Lean 4를 사용하여 연속 함수 계산을 개발하여 Mathlib 라이브러리에 통합하였다. 그들의 방법론은 수학적으로 "순수한" 정의에서 "실용적인" 인터페이스로 나아가는 반복적인 설계 과정을 포함한다. 주요 설계 결정은 다음과 같다:

1. 언번들링(Unbundling) 및 "정크 값(Junk Values)":
   함수 계산을 $C(\sigma(a), \mathbb{C})$ 상의 연속 함수 타입에서 대수로 가는 맵으로 정의하는 대신, 저자들은 임의의 함수 $f: \mathbb{C} \to \mathbb{C}$와 원소 $a$를 받아들이는 함수 cfc를 정의하였다. 만약 $a$가 정규(normal)가 아니거나 $f$가 스펙트럼 위에서 연속이 아니라면, 이 함수는 "정크 값"(통상적으로 0)을 반환한다.

   • 근거: 이를 통해 사용자는 $a$가 정규임을 먼저 증명하거나 $f$가 연속임을 먼저 증명하지 않고도 $f(a)$와 같은 표현식을 작성할 수 있다. 이는 비논리적인 수학의 "먼저 쓰고 나중에 생각하기" 접근 방식을 모방하며, 비자명한 성질이 필요할 때까지 증명의 부담을 유예한다. 또한, 인자의 타입이 더 이상 $a$의 특정 성질에 의존하지 않게 함으로써 원활한 재작성(rw)을 가능하게 한다.

2. 클래스 기반 추상화(Class-Based Abstraction):
   서로 다른 스칼라 환($\mathbb{C}$, $\mathbb{R}$, $\mathbb{R}_{\ge 0}$)과 서로 다른 원소 유형(정규, 자기 수반, 비음수)을 처리하기 위해, 저자들은 함수 계산을 ContinuousFunctionalCalculus라는 타입 클래스로 구현하였다.

   • 술어 일반화: 이 클래스는 대수의 원소에 대한 술어 $p$(예: IsStarNormal, IsSelfAdjoint, 0 ≤ a)에 의해 매개변수화된다. 이를 통해 단일 인터페이스가 코드 중복 없이 다양한 사례를 포괄할 수 있다.
   • Prop-Valued vs. Data: 초기 버전에는 $*$-준동형 사상( $*$-homomorphism)을 데이터로 포함하였다. 그러나 두 가지 서로 다른 구성이 동일한 맵에 대해 정의적 동등성(definitional equality)을 갖지 못할 수 있는 문제를 피하기 위해, 최종 설계에서는 이 클래스를 Prop으로 만들었다. 즉, 이 클래스는 특정 성질을 가진 유일한 $*$-준동형 사상의 존재를 단언할 뿐, 맵 자체를 저장하지 않는다.

3. 비단위 대수(Non-Unital Algebras) 처리:
   본 형식화는 비단위 $C^*$-대수로 확장된다. 모든 정의마다 최소 단위화(minimal unitization)와 같은 외적 구성을 사용하는 대신, 저자들은 **준스펙트럼(quasispectrum)**의 내적 정의를 도입하였다. 비단위 함수 계산은 0에서 0으로 매핑되거나 0에서 사라지는 함수들에 대해 정의되며, 이를 통해 단위 대수와 비단위 대수의 맥락을 끊임없이 전환해야 하는 필요성을 피한다.

4. autoParam을 통한 자동화:
   연속성과 정규성 증명을 수동으로 전달하는 번거로움을 완화하기 위해, 저자들은 Lean의 autoParam 기능을 활용하였다. "f는 스펙트럼 위에서 연속이다"와 같은 가설들은 기본 탭택(tactic)을 갖는다. 사용자가 증명을 제공하지 않으면, Lean은 기존의 렘마(예: aesop, fun_prop)를 사용하여 이를 자동으로 합성하려고 시도한다.

5. 별도의 클래스로서의 유일성(Uniqueness):
   합성 성질($g(f(a)) = (g \circ f)(a)$)은 이론의 핵심이다. 저자들은 Stone–Weierstrass 정리(이는 $\mathbb{R}_{\ge 0}$에 대해 실패함)를 사용하는 대신 유일성 논증을 사용하여 이를 증명하였다. 그들은 $*$-준동형 사상의 유일성을 별도의 클래스인 ContinuousMap.UniqueHom에 캡슐화하여, 합성 성질이 서로 다른 스칼라 환에 걸쳐 일반적으로 유도될 수 있도록 하였다.

주요 기여 및 결과

• 최초의 형식화: 본 연구는 임의의 증명 보조기에서 연속 함수 계산을 최초로 형식화한 것이다.
• Mathlib 통합: 이 구현은 Mathlib에 병합되어 복잡한 실수, 복소수 및 비음수 실수 함수 계산을 위한 통합 인터介이스를 제공한다.
• 사용성 검증: 설계는 다음을 포함한 특정 "리트머스 테스트"를 통해 검증되었다:
  • 모든 곳에서 연속적이지 않은 함수(예: $x \mapsto x^{-1}$)를 사용하여 역원($f(a^{-1})$) 정의하기.
  • 자기 수반 및 비음수 원소에 대한 양의 부분(positive part) 및 제곱근 구성하기.
  • $\mathbb{R}$ 상의 행렬(Mathlib 내에서 전역적 메트릭 구조가 없는)에 함수 계산 적용하기.
• 자동화: 인터페이스는 고수준 자동화를 지원하여, 사용자가 최소한의 수동 개입으로 $f(-a) = (x \mapsto f(-x))(a)$와 같은 성질을 증명할 수 있게 한다.
• 응용: 이 인터페이스는 이미 다음과 같은 고급 결과들을 형식화하는 데 사용되었다:
  • 비단위 $C^*$-대수에서 근사 단위(approximate units)의 존재성.
  • 두 변수 모두에 대한 함수 계산의 연속성.
  • 맵 $a \mapsto |a|$, $a \mapsto a^p$, $a \mapsto \log(a)$에 관한 성질.
  • 유니터리 원소 및 투영(projections)에 관한 결과.

의의 및 한계
본 논문은 그 의의를 주로 설계 철학에서 찾는다. 즉, 대규모 형식 라이브러리에서 도구가 효과적이려면, 정의의 엄격한 수학적 순수성보다 엔드 유저의 편의성(사용성)을 우선시해야 함을 보여준다는 점이다. "정크 값"을 수용하고 타입을 언번들링함으로써, 저자들은 수학자들에게 직관적으로 작동하는 인터페이스를 구축하였으며, 이를 통해 엄격한 의존 타입 접근법으로는 불가능했을 복잡한 조작(합성 및 재작성 등)을 가능하게 하였다.

저자들은 현재 상태에 대해 겸허하게 인정하며 몇 가지 한계를 언급하였다:

• Simp 렘마: autoParam을 트리거하기 위해 명시적 인자가 필요하기 때문에, 많은 렘마들이 수동 개입 없이는 simp 규칙으로 사용될 수 없어 일부 증명이 의도보다 장황해질 수 있다.
• $\mathbb{R}_{\ge 0}$의 복잡성: 비음수 실수(non-negative reals)를 스칼라 환으로 사용하는 것은 특정 기술적 난제(예: 절단된 뺄셈, 링 구조의 부재)를 도입하며, 이는 별도의 정리 문장이 필요하다.
• 실 $C^*$-대수: 본 프레임워크는 실 $C^*$-대수를 지원하도록 설계되었으나, 실 대수에 대한 복소수 상의 함수 계산(다른 영역의 함수를 요구함)의 구체적인 케이스는 아직 완전히 통합되지 않았으며 향후 과제로 남아 있다.

결론적으로, 이 논문은 깊이 있는 연산자 대수 이론을 사용 가능한 형식 시스템으로 성공적으로 번역한 과정을 기록하고 있으며, 상호작용적 정리 증명(interactive theorem proving)의 맥락에서 수학적 우아함과 실용적 유용성 사이의 절충안을 강조하고 있다.