The continuous functional calculus in Lean

Technical Summary: The Continuous Functional Calculus in Lean

Problem Statement
The continuous functional calculus is a foundational tool in the theory of $C^*$-algebras, allowing for the identification of commutative $C^*$-subalgebras with algebras of continuous functions on compact Hausdorff spaces. While mathematically well-understood, its formalization in proof assistants like Lean presents significant challenges. The primary difficulty lies in balancing mathematical fidelity with usability. A "natural" mathematical definition often relies on dependent types (e.g., functions defined only on the spectrum of an element) and bundled structures (e.g., continuous maps as a specific type). While these are rigorous, they create friction in formal proofs: rewriting equalities becomes difficult because types depend on specific elements, and composing functions requires managing complex subtype coercions and continuity proofs. The authors identified that a design prioritizing strict mathematical simplicity often fails the "litmus tests" of practical usability required for a library like Mathlib.

Methodology and Design Decisions
The authors developed a formalization of the continuous functional calculus in Lean 4, integrated into the Mathlib library. Their methodology involved an iterative design process, moving from a mathematically "pure" definition to a "utilitarian" interface. Key design decisions include:

1. Unbundling and "Junk Values":
   Instead of defining the functional calculus as a map from the type of continuous functions on the spectrum $C(\sigma(a), \mathbb{C})$ to the algebra, the authors defined a function cfc that accepts any function $f: \mathbb{C} \to \mathbb{C}$ and any element $a$. If $a$ is not normal or $f$ is not continuous on the spectrum, the function returns a "junk value" (typically 0).

   • Rationale: This allows users to write expressions like $f(a)$ without first proving $a$ is normal or that $f$ is continuous. It mimics the "write first, think later" approach of informal mathematics, delaying the burden of proof until a non-trivial property is needed. This also enables seamless rewriting (rw) because the types of the arguments no longer depend on the specific properties of $a$.

2. Class-Based Abstraction:
   To handle different scalar rings ($\mathbb{C}$, $\mathbb{R}$, and $\mathbb{R}_{\ge 0}$) and different element types (normal, self-adjoint, non-negative), the authors implemented the calculus as a type class ContinuousFunctionalCalculus.

   • Predicate Generalization: The class is parameterized by a predicate $p$ on the algebra elements (e.g., IsStarNormal, IsSelfAdjoint, 0 ≤ a). This allows a single interface to cover various cases without code duplication.
   • Prop-Valued vs. Data: Early versions included the $*$-homomorphism as data. However, to avoid issues with definitional equality (where two different constructions of the same map might not be definitionally equal), the final design makes the class a Prop. It asserts the existence of a unique $*$-homomorphism with specific properties, rather than storing the map itself.

3. Handling Non-Unital Algebras:
   The formalization extends to non-unital $C^*$-algebras. Instead of relying on extrinsic constructions like the minimal unitization for every definition, the authors introduced an intrinsic definition of the quasispectrum. The non-unital functional calculus is defined on functions vanishing at 0 (or mapping 0 to 0), avoiding the need to constantly switch between unital and non-unital contexts.

4. Automation via autoParam:
   To mitigate the verbosity of passing continuity and normality proofs manually, the authors utilized Lean's autoParam feature. Hypotheses such as "f is continuous on the spectrum" are equipped with default tactics. If the user does not provide a proof, Lean attempts to synthesize it automatically using existing lemmas (e.g., aesop, fun_prop).

5. Uniqueness as a Separate Class:
   The composition property ($g(f(a)) = (g \circ f)(a)$) is central to the theory. The authors proved this using a uniqueness argument rather than the Stone–Weierstrass theorem (which fails for $\mathbb{R}_{\ge 0}$). They encapsulated the uniqueness of $*$-homomorphisms in a separate class ContinuousMap.UniqueHom, allowing the composition property to be derived generically across different scalar rings.

Key Contributions and Results

• First Formalization: This work constitutes the first formalization of the continuous functional calculus in any proof assistant.
• Mathlib Integration: The implementation is merged into Mathlib, providing a unified interface for complex, real, and non-negative real functional calculi.
• Usability Verification: The design was validated against specific "litmus tests," including:
  • Defining inverses ($f(a^{-1})$) using functions not continuous everywhere (e.g., $x \mapsto x^{-1}$).
  • Constructing positive/negative parts and square roots for self-adjoint and non-negative elements.
  • Applying the calculus to matrices over $\mathbb{R}$ (which lack a global metric structure in Mathlib).
• Automation: The interface supports high-level automation, allowing users to prove properties like $f(-a) = (x \mapsto f(-x))(a)$ with minimal manual intervention.
• Applications: The interface has already been used to formalize advanced results, including:
  • The existence of approximate units in non-unital $C^*$-algebras.
  • The continuity of the functional calculus in both variables.
  • Properties of maps $a \mapsto |a|$, $a \mapsto a^p$, and $a \mapsto \log(a)$.
  • Results regarding unitary elements and projections.

Significance and Limitations
The paper claims significance primarily in its design philosophy: demonstrating that for a tool to be effective in a large-scale formal library, it must prioritize the ergonomics of the end-user (usability) over strict mathematical purity in the definition. By accepting "junk values" and unbundling types, the authors created an interface that behaves intuitively for mathematicians, allowing for complex manipulations (like composition and rewriting) that would be prohibitively difficult with a strictly dependent-type approach.

The authors are modest about the current state, acknowledging several limitations:

• Simp Lemmas: Due to the need for explicit arguments to trigger autoParam, many lemmas cannot be used as simp rules without manual intervention, making some proofs more verbose than desired.
• $\mathbb{R}_{\ge 0}$ Complications: The use of the non-negative reals as a scalar ring introduces specific technical hurdles (e.g., truncated subtraction, lack of ring structure) that require separate theorem statements.
• Real $C^*$-algebras: While the framework is designed to support real $C^*$-algebras, the specific case of the functional calculus over $\mathbb{C}$ for real algebras (which requires a different domain of functions) is not yet fully integrated and is planned for future work.

In conclusion, the paper documents a successful translation of a deep operator algebra theory into a usable formal system, highlighting the trade-offs between mathematical elegance and practical utility in the context of interactive theorem proving.