Paper release: r1542 Released: July 15, 2026

Keywords: quantum probability, event algebras, Born rule, Lüders conditioning, conditional expectation, Tsirelson bound, formalized mathematics, Lean 4, Mathlib

Mathematics Subject Classification (2020): Primary 81P15, 68V20; Secondary 81P40, 46L53, 81P10.

Introduction

Finite-dimensional event algebras support a complete and elementary account of quantum probability. Over the matrix algebra \(\mathrm{M}_n(\mathbb C)\), events are orthogonal projections, states are density matrices, the Born weight of an event under a state is a trace pairing, conditioning is the Lüders update , classicality is captured by commutative subalgebras and coarse-graining onto a measurement context by a trace-preserving pinching, and the characteristic nonclassical phenomenon, the violation of the CHSH inequality up to Tsirelson’s bound , is already visible for \(4 \times 4\) matrices. Every object in this list is finite-dimensional linear algebra; no unbounded operators, no measure theory, and no functional-analytic subtleties intervene. This elementary core is also where much of the current foundational discussion lives: the status and derivation of the Born rule , the relation between quantum phenomena and Kolmogorov probability , and the derivability of the von Neumann–Lüders measurement postulate remain active topics, including in this journal.

Published treatments of this core, from von Neumann onward, leave the bookkeeping informal. Which statements require positivity of the state, which require only hermiticity, and which are identities of the trace calculus valid for arbitrary matrices? What exactly happens when one conditions on an event of weight zero? Is orthogonality of projections a symmetric hypothesis or a symmetric conclusion? Where, precisely, does the trace enter, and where does pure \(*\)-algebra suffice? In informal mathematics these questions are resolved silently, case by case, by the reader. A proof assistant forces every such choice into the open and then certifies the result.

To the author’s knowledge (search current as of July 2026), this is the first Lean 4 development to package this specific combination: finite projective-event closure lemmas, a Lüders fixed-point / one-step-retraction characterization, the partition-pinching expectation with its Hilbert–Schmidt characterization, and a norm-form CHSH/Tsirelson bound, under a per-declaration axiom audit. Concretely, the development delivers:

1. 64 lemmas and 8 definitions, in Lean 4 over Mathlib , with no sorry placeholders and no axioms beyond Lean’s standard classical base;

2. an axiom audit embedded in the source: every lemma is followed by a #print axioms command, so a complete per-declaration audit re-executes on every build; no theorem depends on axioms outside Lean and Mathlib’s standard classical base [propext, Classical.choice, Quot.sound], and individual dependency sets are subsets of this base (for example, the CHSH ring identity chshmulself is choice-free, reporting [propext, Quot.sound]);

3. a tagging discipline under which every lemma is classified in its documentation string as algebra-only (content provable in the \(*\)-algebra, with norm structure where relevant) or trace-dependent (content passing through the trace pairing \((\rho,P) \mapsto \operatorname{Tr}(\rho P)\)); trace-dependent statements divide further according to whether they additionally require positivity or state-normalization, which is visible in each statement’s hypotheses;

4. the Lüders update packaged with repeatability, idempotence, composition on commuting events, the classical restriction, and a fixed-point characterization identifying the fixed states of conditioning with the states certain of the event;

5. the trace-preserving pinching onto the block-diagonal commutant \(N\) of a projective partition of unity, with a Hilbert–Schmidt characterization: projector, state-preserving, trace-selfadjoint, Pythagorean, contractive, trace-compatible, unique among commutant-valued trace-compatible maps, and compatible with Lüders conditioning on commutant events;

6. the Tsirelson bound in operator-norm form, proved in an abstract unital C*-setting that assumes neither completeness nor any order structure, with the exact ring identity underlying it isolated as a standalone lemma, an instantiation to finite matrix algebras, and an interface lemma reusing Mathlib’s existing CHSH hypothesis bundle.

The development builds with the toolchain leanprover/lean4:v4.29.1 and the Mathlib version pinned to match; it imports Mathlib and nothing else.

Three scope limitations should be stated at the outset. First, the novelty claim above is deliberately narrow and organizational. Formalizations of projective measurement, the Born rule for projective effects, and the CHSH/Tsirelson inequality already exist, in the Isabelle/HOL ecosystem (in particular the work of Echenim and Mhalla ) and in the Lean ecosystem (Mathlib’s order-form CHSH bound and the Physlib/QuantumInfo project ); we make no claim of first formalization for any of those individual results. The contribution here is the organization of the finite core around a projective partition with its trace-preserving pinching onto the block-diagonal commutant, the lemma-by-lemma separation of algebra-only from trace-dependent content, the abstract C*-setting of the norm-form bound, and the prover ecosystem. Second, no attainment or tightness statement for the Tsirelson bound is formalized: the development ships the inequality only. Third, everything is finite-dimensional; extensions toward infinite dimensions are discussed as outlook in Section 11.

Finite event algebras arise, for example, as the measurement cores of finite models of quantum theory. Beyond that single remark, this paper is self-contained: Section 2 fixes the mathematical setting, Section 3 describes the architecture and conventions of the formalization, Sections 4 through 8 walk through the five modules with the main statements as numbered propositions carrying their Lean names, Section 9 documents Mathlib gaps and proof engineering, Section 10 discusses related work, and Section 11 concludes.

Mathematical setting

Throughout, \(n\) and \(k\) denote natural numbers and \(\mathrm{M}_n(\mathbb C)\) denotes the \(*\)-algebra of \(n \times n\) complex matrices, with conjugate transpose \(X \mapsto X^{*}\), trace \(\operatorname{Tr}\), identity \(\mathbf 1\), and zero \(0\). All statements below are formalized for every \(n\), including the degenerate case \(n = 0\); only the matrix instantiation of the Tsirelson bound (Proposition 20) assumes \(n \neq 0\).

The partial order on \(\mathbb C\) is the one in which \(z \le w\) exactly when \(\operatorname{Re} z \le \operatorname{Re} w\) and \(\operatorname{Im} z = \operatorname{Im} w\); in particular \(0 \le z\) asserts that \(z\) is real and nonnegative. Nonnegativity and boundedness of Born weights are proved below in this partial order, which is strictly stronger than the corresponding assertions about real parts; real-part corollaries are provided alongside each such statement.

Events are exactly the orthogonal projections, the sharp yes/no tests of the finite quantum formalism . The subevent relation is witnessed algebraically: \(P\) is a subevent of \(Q\) when \(PQ = P\).

The weight is defined as a complex number for arbitrary matrix arguments; reality under hermiticity is a theorem (Proposition 3), and the probabilistic bounds hold under the appropriate positivity hypotheses (Proposition 4).

The scalar inverse is taken in \(\mathbb C\) with Lean’s convention \(0^{-1} = 0\), so conditioning on an event of vanishing weight degenerates to the zero matrix; every substantive lemma about the update carries the explicit guard \(\mu_\rho(P) \neq 0\). The rule goes back to Lüders ; see Busch and Lahti for its place in the measurement literature.

The members of a projective partition commute pairwise (Proposition 11), so they generate a commutative unital \(*\)-subalgebra \[ D \coloneqq \operatorname{span}\{P_i : i < k\} \subseteq \mathrm{M}_n(\mathbb C). \] The associated commutant is the block-diagonal algebra \[ N \coloneqq \pi' \coloneqq \{\, X \in \mathrm{M}_n(\mathbb C): X P_i = P_i X \text{ for all } i < k \,\} \;\cong\; \bigoplus_{i < k} \mathrm{M}_{\operatorname{rank} P_i}(\mathbb C), \] which is in general noncommutative. The commutative algebra \(D\) is exactly the center of the commutant, \(D = Z(N)\): the block-scalar matrices. This is the one precise sense in which a “center” figures here. As the next definition records, the pinching lands in \(N\), not in \(D\).

Section 6 verifies that \(\mathcal E_\pi\) is the trace-preserving conditional expectation onto the commutant \(\pi'\), with the Hilbert–Schmidt characterization: it is a projector onto \(\pi'\), maps states to states, is selfadjoint for the trace inner product \(\langle X,\,Y\rangle = \operatorname{Tr}(X^{*}Y)\), satisfies the Pythagorean identity, contracts the squared trace norm, is uniquely determined by trace compatibility, and commutes with Lüders conditioning on commutant events. When the partition is rank one, so that every \(P_i\) has rank one, the commutant \(\pi'\) coincides with \(D\) and \(\mathcal E_\pi\) is the classical conditional expectation onto \(D\).

Finally, the CHSH combination. In a unital C*-algebra \(A\), take selfadjoint involutions \(a_0, a_1, b_0, b_1\) (each equal to its own star, each squaring to \(\mathbf 1\)) such that every \(a_i\) commutes with every \(b_j\), and form \[ S \coloneqq a_0 b_0 + a_0 b_1 + a_1 b_0 - a_1 b_1 . \] Classically, dichotomic \(\pm 1\) observables obey \(\lvert \langle S \rangle \rvert \le 2\) ; quantum mechanically the sharp bound is Tsirelson’s \(\lVert S\rVert \le 2\sqrt{2}\) . The bridge from the event layer to these hypotheses is the dichotomic observable \(\mathbf 1- 2P\) of an event \(P\), which is a selfadjoint involution (Proposition 1(ix)).

The formalization: architecture and conventions

Modules

The development consists of five modules under a single namespace, importing Mathlib and nothing else:

The event and state layers are formalized over the concrete carrier Matrix (Fin n) (Fin n) \(\mathbb C\). This choice trades generality for the density of Mathlib’s finite matrix API (positive semidefiniteness, trace calculus, spectral theorem), which carries most of the proofs. The Tsirelson module, whose content is norm-theoretic rather than matrix-theoretic, is instead stated over an abstract typeclass context and instantiated to matrices only at the end (Section 8).

Scoped instances

Three pieces of structure that the development relies on are scoped in Mathlib rather than globally active, and must be opened explicitly:

• ComplexOrder: the partial order on \(\mathbb C\) of Section 2, together with the ordered-ring structure that makes products of nonnegative complex numbers nonnegative;

• MatrixOrder: the Loewner order on matrices;

• Matrix.Norms.L2Operator: the \(L^2\) operator norm on \(\mathrm{M}_n(\mathbb C)\) together with its normed-ring and C*-identity instances. There is no globally installed norm on the matrix type, so the matrix instantiation of the Tsirelson bound lives behind this scope.

Section 9 discusses the practical consequences of this scoping.

The algebra-only/trace-dependent split

Every lemma in the development carries one of two tags in its documentation string:

• algebra-only: the content is pure \(*\)-algebra (ring and star structure; in the Tsirelson module, also norm structure), consuming no state and no trace functional;

• trace-dependent: the content passes through the trace pairing \((\rho, P) \mapsto \operatorname{Tr}(\rho P)\); trace-dependent statements divide further by whether they also require positivity or state-normalization, which is visible in each statement’s hypotheses.

The split is a statement-classification discipline rather than an import boundary: it makes visible, lemma by lemma, exactly where probabilistic content enters the theory. All event-closure lemmas, the entire partition algebra, the projector laws of the pinching map, and the entire Tsirelson module are algebra-only; every statement about Born weights, updates of states, and trace inner products consumes the trace. In the propositions below, this classification is reproduced: statements in Sections 4 through 7 are tagged individually, and everything in Section 8 is algebra-only.

Axiom audit and build discipline

Each of the 64 lemmas is followed in the source by a #print axioms command, so the axiom audit is part of the source text and re-executes on every build. No result depends on any axiom outside Lean’s standard classical base \[ \texttt{[propext, Classical.choice, Quot.sound]} \] (propositional extensionality, choice, and quotient soundness); individual dependency sets are subsets of this base. The ring identity chshmulself is choice-free, reporting only [propext, Quot.sound]. The complete declaration-by-declaration audit accompanies the artifact as AXIOMAUDIT.txt. The development contains no sorry placeholders, no custom axioms, and no unfinished obligations; the toolchain is leanprover/lean4:v4.29.1 with Mathlib pinned at the matching version, and the project builds cleanly under lake (8254 jobs).

Proofs in this paper are given as sketches only; the complete formal proofs constitute the accompanying development, and each proposition cites the corresponding Lean names in typewriter font.

Events and Born weights

The first module establishes closure of the event set under the natural logical operations and the probabilistic behavior of the Born weight.

Item (ix) is the bridge from events to the CHSH hypotheses of Section 8: each event answers a yes/no question, and \(\mathbf 1- 2P\) is the associated \(\pm 1\)-valued observable.

Item (iv), the sandwich identity, requires only idempotence of \(P\); hermiticity is never used. It is the workhorse that lets positivity arguments compress the state by the event and is applied throughout the conditioning module.

Together, Propositions 1 and 4 verify that \(P \mapsto \mu_\rho(P)\) is a finitely additive, normalized, monotone probability assignment on events, with reality and the bounds stated in the strong (\(\mathbb C\)-order) form. Item (vi) is the exact interface later needed by the conditioning guards.

Lüders conditioning

The second module packages the Lüders update as a state transformer and proves its characteristic laws. A remark on hypothesis minimality is in order: because the formal statements register exactly what each proof uses, several conditioning identities below hold for an arbitrary matrix \(\rho\), with state hypotheses appearing only where positivity or normalization genuinely enters.

By Proposition 4(vi), the guard \(\mu_\rho(P) \neq 0\) is equivalent, for positive-semidefinite \(\rho\), to the weight having strictly positive real part.

Neither positivity nor normalization of \(\rho\) is used: repeatability is an identity of the trace calculus, valid for every matrix \(\rho\) subject to the guard.

In the commuting case the Lüders update is the normalized restriction, which is the formula of classical conditional probability; quantum conditioning strictly extends the classical rule.

Conditioning as a one-step retraction onto its fixed points

Repeatability and idempotence assemble into a fixed-point description of measurement update.

Trace-preserving pinching onto the block-diagonal commutant

The third module is the organizational core of the development. A projective partition \(\pi = (P_i)_{i<k}\) (Definition 5) plays the role of a measurement context; the pinching \(\mathcal E_\pi\) (Definition 6) is verified to be the trace-preserving conditional expectation onto the block-diagonal commutant \(\pi'\), in the precise sense of the uniqueness statement below. The range \(\pi'\) is in general noncommutative, so \(\mathcal E_\pi\) preserves quantum coherence within a degenerate block; it reduces to the classical conditional expectation onto \(D = \operatorname{span}\{P_i\}\) exactly when the partition is rank one.

This is the quantum counterpart of the classical \(L^2\) energy identity for conditional expectations: the pinching is the orthogonal projection, for the trace inner product, onto the commutant of the context.

Item (i) is the defining property of a conditional expectation, and (ii) says the pinching is the only commutant-valued map with that property: existence and uniqueness are both machine-checked.

Item (i) guarantees that the normalizing scalars on both sides of (ii) agree, so the exchange law holds at the level of matrices, degenerate cases included. Conditioning on commutant events therefore commutes with the pinching onto \(\pi'\). In the rank-one case, where \(\pi' = D\) is commutative, this is exactly the classical statement that conditioning interacts with a sub-\(\sigma\)-algebra through the conditional expectation; in general it is the block-diagonal refinement of that statement.

The expectation functional

The fourth module attaches to each state its expectation functional on observables and proves that it is a positive normalized linear functional, strengthening Born-weight positivity from events to arbitrary positive-semidefinite observables.

The Tsirelson bound

The fifth module is entirely algebra-only: no state and no trace appear anywhere in it. Its content splits into an exact ring identity, two C*-norm lemmas, the abstract bound, and interoperability statements.

The ring identity

The identity involves no star, no order, and no norm: it is the exact algebraic content of the Tsirelson bound, stated in a bare ring. The sign convention is that of commutators \([x,y] = xy - yx\), with the minus sign in front of the product of commutators. As noted in Section 3, this lemma’s axiom audit reports only [propext, Quot.sound]. Its proof engineering, a hand-rolled confluent rewrite system standing in for a missing noncommutative tactic, is described in Section 9.

The norm bound

The analytic half runs in an abstract typeclass context: a normed ring carrying a star-ring structure satisfying the C*-identity \(\lVert x^{*}x\rVert = \lVert x\rVert^2\), and nontrivial (so that \(\lVert \mathbf 1\rVert = 1\)). In Lean the hypotheses are the typeclasses \[ [\texttt{NormedRing } A]\ [\texttt{StarRing } A]\ [\texttt{CStarRing } A]\ [\texttt{Nontrivial } A]. \] Neither completeness nor any order structure on \(A\) is assumed; in particular no ambient CStarAlgebra bundle is required.

No attainment or tightness statement is formalized anywhere in the module: the development ships the bound as an inequality, and nothing in it asserts that \(2\sqrt 2\) is achieved.

Relation to Mathlib’s CHSH file and the matrix instantiation

Mathlib already contains an order-theoretic form of the Tsirelson inequality: the file Mathlib/Algebra/Star/CHSH proves, in a star-ordered algebra over the reals, that the CHSH combination satisfies \(S \le 2\sqrt{2} \cdot \mathbf 1\) in the algebra’s order, together with the hypothesis bundle IsCHSHTuple packaging selfadjointness, involutivity, and the cross commutations. The present development contributes the complementary norm-form statement in the C*-setting, with the underlying algebraic identity isolated as Proposition 18, and connects the two through the shared interface:

Item (ii) returns the abstract statement to the ambient algebra of the event-algebra modules; combined with Proposition 1(ix), any four events with the appropriate commutation pattern yield dichotomic observables to which the bound applies. Because the abstract theorem is typeclass-generic, the matrix case is an instantiation of a few lines rather than a separate proof; the only genuine work is a hand-constructed nontriviality instance for the matrix algebra (Section 9).

Mathlib gaps and proof engineering

This section reports the friction points and affordances encountered against the pinned Mathlib version, as raw material for library builders and for others formalizing quantum-probabilistic content.

Scoped instances

Three layers of structure needed by this development are scoped. The partial order on \(\mathbb C\) requires open scoped ComplexOrder; without it, goals mentioning \(0 \le z\) or Matrix.PosSemidef over \(\mathbb C\) fail to elaborate, with instance errors that do not point to the missing scope. The Loewner order on matrices is likewise scoped (MatrixOrder), as is the ordered-ring structure on \(\mathbb C\) that supplies mulnonneg in the complex order. Most consequentially, there is no globally installed norm on the matrix type: the \(L^2\) operator norm and its NormedRing and CStarRing instances activate only under open scoped Matrix.Norms.L2Operator, so the matrix instantiation of Theorem 1 must live behind that scope. In the same corner, no Nontrivial instance fired for the matrix algebra, and nontriviality (needed for \(\lVert \mathbf 1\rVert = 1\)) had to be constructed by hand, entrywise, from \(n \neq 0\). The scoping policy is defensible library design, since competing orders and norms exist on the same types; downstream, it is a real usability tax, and the failure modes when a scope is missing are hard to diagnose.

Positivity of the trace pairing

Mathlib provides \(\operatorname{Tr}M \ge 0\) for a single positive-semidefinite matrix and covers sandwiches \(B A B^{*}\) of positive-semidefinite matrices, yet the bilinear statement, \(\operatorname{Tr}(AB) \ge 0\) for positive-semidefinite \(A\) and \(B\), is absent. For Born weights this is harmless: an event is idempotent, so \(\operatorname{Tr}(\rho P) = \operatorname{Tr}(P \rho P)\) by cycling the trace, and the single-matrix lemma applies. For the expectation functional (Proposition 17(iv)) there is no idempotent to compress with, and the natural abstract route failed in an instructive way. Mathlib’s Gram-factorization characterization of positivity, CStarAlgebra.nonnegiffeqstarmulself combined with the Loewner-order bridge Matrix.PosSemidef.nonneg, is gated behind the continuous functional calculus, and instance synthesis for two of its classes, NonUnitalContinuousFunctionalCalculus over \(\mathbb R\) with the IsSelfAdjoint predicate and NonnegSpectrumClass over \(\mathbb R\), did not resolve for the matrix algebra carrying the Pi topology, even with the order scopes open. (Mathlib’s own matrix-order file uses the lemma successfully inside its own section context; the instance chain did not reproduce downstream for us.) The workaround is elementary and robust: decompose spectrally via Matrix.IsHermitian.spectraltheorem, extract nonnegative eigenvalues with PosSemidef.eigenvaluesnonneg, cycle the trace, and sum termwise; about a dozen lines.

No noncommutative linearcombination

The CHSH square identity (Proposition 18) is pure noncommutative-ring algebra with side relations: involutivity of the four letters and the four cross commutations. Lean’s linearcombination tactic is commutative-only, and noncommring normalizes without consuming hypotheses, so neither closes the goal. The formal proof instead builds a small confluent rewrite system by hand: from each commutation hypothesis it derives the association-compatible, universally quantified form \(b\,(a\,x) = a\,(b\,x)\), and from each involution the cancellation form \(a\,(a\,x) = x\); running these as a simp only set over right-associated words moves every \(b\) past every \(a\) and cancels adjacent equal letters, and abel finishes the additive bookkeeping. The system terminates because each rewrite strictly decreases the number of letters out of normal order. A noncommutative analogue of linearcombination, even one restricted to rewriting modulo hypothesis-supplied commutation and involution relations, would compress this style of proof considerably.

Occurrence-sensitive rewriting

A recurring low-level friction: on goals containing several syntactic occurrences of the same subterm, rw rewrites the first occurrence, which in conditioning goals is typically the normalizing scalar \((\mu_\rho(P))^{-1}\) rather than the intended trace argument. The stable pattern was to isolate each trace identity as a standalone have with explicit arguments to tracemulcomm or tracemulcycle, and only then rewrite. A minor lexical note in the same spirit: the script capital letter often used for partitions in informal notation is outside Lean’s legal identifier alphabet in this toolchain, so partition variables are plain ASCII.

Affordances

Three parts of Mathlib made the development markedly shorter than a bespoke stack would be. First, the Matrix.PosSemidef API is definition-agnostic: sandwich closure in both directions (PosSemidef.mulmulconjTransposesame, PosSemidef.conjTransposemulmulsame), sums (posSemidefsum), scalar multiples (PosSemidef.smul, which accepts a complex scalar that is nonnegative in the complex order, so the Lüders normalization is a single application), diagonal nonnegativity, trace nonnegativity, the zero-trace criterion, and the Gram construction posSemidefconjTransposemulself covered every need without ever unfolding the definition. Second, trace faithfulness is in the box: Matrix.tracemulconjTransposeselfeqzeroiff powers the uniqueness of the center expectation, and PosSemidef.traceeqzeroiff together with PosSemidef.dotProductmulVeczeroiff powers the support lemma of Proposition 10(ii). Third, the C*-norm layer, CStarRing.normstarmulself, IsSelfAdjoint.normmulself, the norm-one instance for nontrivial C*-rings, and normnsmulle, reduces the analytic half of Theorem 1 to roughly forty lines over the bare typeclass context, with no completeness assumption anywhere. Mathlib’s existing CHSH file was itself an affordance: its IsCHSHTuple bundle fixed the interface against which the norm-form result could be made interoperable from the start.

Related work

The Isabelle/HOL line. The nearest prior art is the sequence of developments by Echenim and Mhalla. Echenim’s Archive of Formal Proofs entry on quantum projective measurements and the CHSH inequality formalizes projective measurements and the CHSH expectation in Isabelle/HOL; the journal treatment by Echenim and Mhalla presents a formalization of the CHSH inequality and Tsirelson’s upper bound, with the corresponding AFP entry ; a supporting AFP entry formalizes simultaneous diagonalization of pairwise commuting Hermitian matrices . Relative to that line, the present development differs on two axes. Organizationally, it is event-algebra-first: the theory is arranged around the closure algebra of Hermitian idempotents, the block-diagonal commutant with an explicit trace-preserving pinching carrying existence, uniqueness, and contractivity, and a lemma-by-lemma, machine-visible split between algebra-only and trace-dependent content; the Isabelle line is organized matrix-first over a concrete density-matrix and \(L^2\)-norm stack, with the CHSH development as the target. On the prover axis, the ecosystems differ in a way that shows up in proof economy: in Lean/Mathlib the norm-form Tsirelson bound is proved abstractly for any nontrivial unital C*-ring, with the matrix case a short instantiation, and Born-weight positivity and boundedness live directly in the partial order of \(\mathbb C\) with no bespoke real-part bookkeeping; conversely, the concrete Isabelle stack obtains from its own spectral toolbox some facts (such as Gram factorization of positive matrices) that are currently gated behind unresolved instance chains in Mathlib, as detailed in Section 9. The CHSH arithmetic itself is common ground; the organization is the delta.

Formalized quantum mathematics more broadly. Bordg, Lachnitt, and He verified quantum algorithms and information-theoretic results in Isabelle/HOL , with the accompanying Isabelle Marries Dirac library . In Lean/Mathlib, Dupuis, Lewis, and Macbeth developed formalized functional analysis with semilinear maps , infrastructure relevant to any future infinite-dimensional extension of the present work. Garrigue and Saikawa formalize typed compositional quantum computation with lenses . Reports on individual Mathlib formalization efforts, such as Nash on Engel’s theorem and Baanen and collaborators on Dedekind domains and class groups of global fields , document both the mathematics and the practice of folding formalization-driven contributions back into the library; the library itself is described in the Mathlib community paper , and the Lean 4 system in de Moura and Ullrich . Within Lean specifically, Mathlib already provides an order-form CHSH/Tsirelson inequality and the IsCHSHTuple interface used in Section 8, and the Physlib/QuantumInfo project formalizes finite mixed states as positive-semidefinite trace-one matrices, positive operator-valued measures, and a Born-rule measurement. Relative to these, the present development contributes the event-algebra organization, the commutant pinching with its Hilbert–Schmidt characterization, the Lüders fixed-point layer, and the norm-form CHSH bound, packaged together under a per-declaration axiom audit; the novelty claim of Section 1 is exactly this specific combination.

Foundations context. The mathematical foundations of quantum probability remain under active discussion in this journal’s scope. Reddiger and Poirier examine the one-body Born rule in curved spacetime ; Reddiger analyzes the applicability of Kolmogorov’s probability theory to quantum phenomena ; Aharonov and Shushi revisit the derivation of the Born rule , and Beck surveys the textbook orthodoxy on measurement and state update . Arsiwalla, Chester, and Kauffman reconstruct expectation values from a pre-quantum operator algebra, treating classical and quantum wave functions as consequences of that operator layer ; Kumar and Pan study network nonlocality , and Held derives the Tsirelson bound from geometric-algebra assumptions . Goldstein bootstraps infinite-dimensional state spaces from finite ones, deriving the von Neumann–Lüders postulate for projective observables . The present paper contributes to that discussion at the level of certified bookkeeping: for the finite core, every hypothesis of every standard statement is now explicit and machine-audited, so debates about what follows from what can point to a checked artifact.

Conclusion and outlook

The finite event-algebra core of quantum probability admits a complete machine-checked treatment at modest cost: 64 lemmas and 8 definitions cover event closure, Born weights with reality and the probabilistic bounds in the strong complex-order form, repeatable Lüders conditioning with its fixed-point characterization, the trace-preserving pinching onto the block-diagonal commutant with its Hilbert–Schmidt characterization (projector, state-preserving, selfadjoint, Pythagorean, contractive, trace-compatible, unique among commutant-valued trace-compatible maps, and compatible with conditioning on commutant events), a positive normalized expectation functional, and the Tsirelson bound in an abstract C*-setting. The axiom audit is part of the source and re-executes on every build; the lemma-level split between algebra-only and state-consuming content gives the development a second, structural payload beyond the individual theorems: it is a machine-visible map of where probability enters the quantum formalism.

Three extensions are natural. First, unsharp measurements: effects (\(0 \le E \le \mathbf 1\) in the Loewner order) and instruments generalize events and the Lüders map, and the certainty-set and fixed-point interface of Section 5 suggests the shape the generalized statements should take. Second, attainment: complementing Theorem 1 with a formalized two-qubit witness achieving \(2\sqrt 2\) would close the gap between the inequality and the bound’s sharpness, and is well within reach of the matrix instantiation already in place. Third, infinite dimensions: the finite development deliberately avoids completeness, so its Tsirelson theorem already applies to any nontrivial unital C*-ring, yet the event-and-state layer is genuinely finite. Goldstein’s bootstrap of infinite-dimensional state spaces from finite ones in this journal marks exactly the frontier a formal development would next confront: which parts of the finite bookkeeping survive the passage verbatim, and which require new analysis (normality of states, \(\sigma\)-additivity, von Neumann algebras in place of matrix algebras). The conditional-expectation package of Section 6 is the component we expect to generalize most cleanly, since its statements are already phrased against a commutant rather than against matrix entries.

When the bookkeeping of a foundational formalism is mechanical and audited, discussion can concentrate on the questions that are actually open. For finite quantum event algebras, that state has now been reached.

Declarations

Funding. No funding was received for this work.

Competing interests. The author declares no competing interests.

Author contributions. Bernhard Mueller is the sole author: he designed and wrote the Lean development, conducted the axiom audit, and wrote the manuscript.

Data availability. No data were generated or analyzed in this work.

Use of AI tools. The author used AI-assisted tools in drafting the Lean development and the manuscript. All formal statements and proofs were checked by the Lean 4 proof assistant, the axiom audits were machine-executed, and the author reviewed and takes full responsibility for the content.

Code availability. The complete Lean development accompanies the submission as a standalone Lake project with a pinned external Mathlib dependency; it does not vendor Mathlib. It builds free of sorry placeholders with the toolchain leanprover/lean4:v4.29.1 and the Mathlib version pinned in the project manifest, and the complete per-declaration axiom audit re-executes as part of the build. A public release with a persistent identifier and an open-source license will accompany publication.