🔢 mathematics

A Layered Lean 4 Library for Finite-Dimensional Quantum Foundations with Typed Premise Auditing

This paper presents a layered Lean 4 library for finite-dimensional quantum foundations that formalizes key representation theorems and complexity results while introducing a typed premise-audit framework to verify the coherence and validity of conditional mathematical theorems, such as the independence of subspace weights from orthogonal decompositions.

Original authors: Bertrand Dalimier

Published 2026-08-20

📖 5 min read🧠 Deep dive

CC BY 4.0

Original authors: Bertrand Dalimier

Original paper licensed under CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Quantum mechanics is the set of rules that governs the behavior of the very small, from atoms to the particles within them. For decades, physicists have relied on a specific rule, known as the Born rule, to calculate the likelihood of finding a particle in a particular place or state. This rule acts as a bridge between the abstract mathematics of quantum theory and the concrete numbers we observe in experiments. However, a deep question has lingered: can this rule be derived from more fundamental principles, or is it simply a necessary assumption we must accept? To answer this, researchers must examine the logical structure of quantum theory with extreme precision, ensuring that every assumption is necessary and that no hidden shortcuts are being taken. This requires a level of scrutiny that human intuition alone cannot provide, as the mathematical landscape is vast and filled with subtle traps where a small error in logic can lead to a false conclusion.

In a significant step toward clarity, a researcher named Bertrand Dalimier has constructed a massive, digital library of mathematical proofs to explore these foundations. Using a specialized computer language designed for verifying logic, Dalimier built a system that checks thousands of statements about quantum mechanics to ensure they are absolutely true. This work is not about discovering new particles or changing the laws of physics; rather, it is about building a perfectly reliable map of the existing laws. The project focuses on finite-dimensional systems, which are the mathematical models used to describe quantum computers and simple quantum systems, rather than the infinitely complex systems found in continuous space. By creating this library, the author has assembled a toolkit of verified definitions and theorems that other scientists can use without having to rebuild the foundation from scratch every time.

The library contains proofs for several famous results in quantum theory, including theorems that describe how symmetries in the quantum world relate to physical transformations, and how complex measurements can be broken down into simpler parts. One of the most important achievements is the verification of the Born rule under specific conditions. The researcher demonstrated that if certain logical requirements are met—such as the idea that the probability of an event should not depend on how the possible outcomes are grouped together—then the Born rule naturally follows. However, the work also revealed that this derivation is not automatic. The researcher proved that if you remove the requirement that the system must have at least three dimensions, the logic breaks down. In a two-dimensional system, which corresponds to a simple quantum bit or qubit, it is possible to construct a scenario that satisfies all the other logical rules but produces a different probability rule. This finding confirms that the dimension of the system is a crucial piece of the puzzle, not just a technical detail.

To ensure that these proofs are trustworthy, the project includes a unique system for auditing the assumptions. Just as a building inspector checks not only that the walls are straight but also that the foundation is solid, this digital library checks whether the starting assumptions of a theorem are actually necessary. The researcher found that some conditions, which were previously thought to be essential, were actually redundant or "vacuous," meaning they were satisfied by everything and therefore added no real constraint. Conversely, the audit showed that other conditions, like the specific way probabilities must add up when outcomes are combined, are strictly necessary. The work also produced counterexamples, which are specific, constructed scenarios that show what happens when a rule is broken. For instance, the researcher built a specific model for a two-dimensional system that follows all the logical rules except for the dimension requirement, and showed that this model produces probabilities that do not match the standard Born rule.

The project is organized into three interconnected parts, each serving a different purpose. The first part establishes the basic vocabulary, defining what a quantum state, a measurement, and a probability are in a way that a computer can understand. The second part uses this vocabulary to prove the major theorems about symmetry and measurement. The third part applies these results to a specific question about how rational decision-making in a quantum world leads to the Born rule. Throughout this process, the researcher used artificial intelligence tools to help write the code and check the logic, but every single step was reviewed and approved by the human author. The final result is a collection of over 67,000 lines of code, verified by a computer, that stands as a rigorous, error-free record of the logical structure of finite-dimensional quantum mechanics.

This work does not claim to solve every mystery of quantum physics, nor does it extend to infinite systems or unbounded observables. Its power lies in its precision and its transparency. By pinning every definition and theorem to a specific version of the software, the researcher has created a reproducible record that anyone can inspect. The library shows that while the Born rule can be derived from a set of clear, logical principles, those principles are delicate. They require the system to have a certain size and structure, and they fail if any of the core assumptions are relaxed. This digital library serves as a new standard for how quantum foundations can be studied, moving the field from informal arguments to a state where every claim is backed by a machine-checked proof. It offers a clear, unshakeable view of what is known, what is necessary, and where the boundaries of our current understanding truly lie.

Technical Summary: A Layered Lean 4 Library for Finite-Dimensional Quantum Foundations with Typed Premise Auditing

Problem Statement
Formalizing theorems in quantum foundations often requires reconstructing substantial infrastructure—finite-dimensional Hilbert space models, projections, effects, density operators, and trace-based Born values—independently for each development. This duplication leads to incompatible interfaces and redundant proof effort. Furthermore, while interactive theorem provers (like Lean 4) can verify that a proof term inhabits an elaborated type, they do not inherently verify that the premises of a theorem are jointly satisfiable, that quantified test classes are non-degenerate, or that specific assumptions perform the intended discriminating role. The paper addresses the need for a reusable, auditable foundation for finite-dimensional quantum formalizations and a framework to inspect the logical status of conditional premises.

Methodology
The author developed a layered architecture spanning three pinned Lean 4 repositories, totaling approximately 67,908 lines of code across 339 files. The development relies on a shared concrete operator layer using EuclideanSpace C (Fin n) for finite-dimensional complex Hilbert spaces, avoiding abstract infinite-dimensional generalizations to ensure explicit, inspectable witnesses.

The methodology involves three distinct layers:

Representation Layer (Gleason Repository): Defines shared types for projections, effects, density operators, and trace-based Born values. It proves finite-dimensional versions of the Gleason and Busch representation theorems.
Foundational Clients (Quantum Foundations Repository): Builds upon the representation layer to formalize Wigner's theorem, a one-directional Uhlhorn theorem, explicit finite Naimark dilation, Kent's contrary-inferences construction, Riedel's redundant-record decomposition, and circuit-complexity results.
Decision and Audit Clients (Everettian Probability Repository): Introduces interfaces for rational expectation and conditional probability. It applies a "partial typed premise-audit" framework to a conditional Born theorem, systematically checking obligations such as joint satisfiability, vacuity, relative necessity, and premise eliminability.

The audit framework adapts concepts from specification validation (e.g., vacuity) to strongly typed mathematical theorems. It distinguishes between kernel acceptance (formal derivability) and semantic adequacy, using explicit inhabitants, rival models, and counterexamples to test the strength and necessity of premises.

Key Contributions

Layered Library Architecture: The primary contribution is a reusable, versioned collection of finite-dimensional quantum formalizations. The three repositories share a concrete operator vocabulary, allowing downstream developments (symmetry, dilation, complexity, selectors) to reuse definitions and bridge lemmas without repository-specific conversions.
First Formalizations: To the author's knowledge, this work presents the first machine-checked formalizations of:
- Wigner's theorem (vector-level) and a one-directional Uhlhorn theorem (projective level).
- Explicit finite Naimark dilation.
- Kent's contrary-inferences construction.
- Riedel's redundant-record decomposition.
- Circuit-complexity lower bounds derived from redundant records.
Typed Premise Auditing Framework: The paper introduces a method for auditing conditional theorems by explicitly discharging nine obligations: joint satisfiability, domain non-emptiness, discriminating force, relative independence, relative necessity, level-matched non-circularity, vacuity, premise eliminability, and formulation minimality.
Exact Classification Results:
- Binary Implementations: A strict classification of binary implementations of a fixed effect under strict isomorphism, showing equivalence if and only if the dimensions of their residual event and complement sectors agree.
- Circuit Complexity: A lower bound of $\lceil R/2 \rceil$ for the length of exact two-site circuits required to reach a specific cross-amplitude interference threshold when $R$ distinct branches are redundantly recorded on pairwise-disjoint regions.
- Selectors: Exact equivalences separating symmetry (unitary covariance), support (NSNC-1), and composition (tensor multiplicativity) conditions for selectors.

Key Results

Conditional Born Representation: The library proves that if an estimation rule satisfies Grain coherence, normalization, positivity, and state-relative null support (with dimension $n \ge 3$ ), it yields the Born rule. Crucially, the audit demonstrates that Grain coherence alone is sufficient to make a subspace weight independent of the orthogonal decomposition in which it occurs, without requiring normalization.
Dimensional Sharpness: The paper provides explicit countermodels showing that the dimension bound $n \ge 3$ is necessary for the projective Gleason representation and the conditional Born theorem. In dimension two, a "skew" weight rule satisfies all four weight predicates (Grain, normalization, positivity, null support) but disagrees with Born weights. This countermodel is lifted to the level of RationalExpectationFamily to show that decision-theoretic premises alone do not entail Born weights without the dimensional side condition.
Vacuity Detection: The audit identifies that a previously considered "global payoff preservation" premise is vacuous; it restricts the test class to constant acts, rendering the condition automatically satisfied by any rational expectation family without providing discriminating power.
Countermodels: The release includes a ProjMeasure 2 that admits no density-operator representation, proving the sharpness of the Gleason theorem's dimension bound at the exact input type.

Significance and Claims
The paper claims significance primarily as a library engineering contribution and a methodological demonstration, rather than a derivation of quantum probability from first principles or a general solution for all Hilbert spaces.

Reusability: The work establishes that a concrete, finite-dimensional operator layer can support a substantial family of formal results, reducing the need to rebuild foundational infrastructure. The author explicitly states that no upstream priority is claimed for the Gleason or Busch theorems (as independent work exists), but the contribution lies in their coexistence within a reproducible dependency chain with inspectable signatures.
Audit Discipline: The paper argues that kernel checking is insufficient for assessing the evidential force of conditional theorems. The proposed audit framework forces a separation between proof-term dependencies and the logical status of the theorem statement itself (e.g., whether premises are necessary or vacuous).
Modesty of Scope: The author is explicit about limitations:
- The library is restricted to finite-dimensional complex spaces; it does not cover separable infinite-dimensional spaces or countable additivity.
- No external adoption is claimed; interoperability with other abstract Hilbert space representations requires manual transport via isometric equivalence.
- The conditional Born theorem does not derive the Born rule from dynamics or rationality alone; it formalizes an implication from explicit, typed premises.
- The use of AI assistants is acknowledged for proof search and refactoring, but the author retains full responsibility for the selection of definitions, theorem statements, and the interpretation of results.

In summary, the paper presents a reproducible, layered formalization of finite-dimensional quantum foundations that prioritizes interface consistency and the rigorous auditing of theorem premises, providing a toolkit for future formal developments while explicitly delineating the boundaries of its current scope.

Technical Summary: A Layered Lean 4 Library for Finite-Dimensional Quantum Foundations with Typed Premise Auditing

More like this