Machine-Checked Finite Event Algebras for Observer-Patch Holography

Keywords: formal verification, Lean 4, projective measurement, partition pinching, support-aware relative entropy, Lüders update, CHSH

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

Introduction

Finite quantum measurement is short on paper. A proof calls a matrix a state, inserts a projection, normalizes the result, and moves on. Lean asks for every condition skipped in that sentence. The matrix must be positive and have unit trace. The projection must be Hermitian and idempotent. Normalization needs a nonzero denominator. Later norm estimates require a further set of instances.

Machine-checked quantum information is an active area, spread over several systems and several design philosophies. Mathlib [source], the central mathematics library of Lean 4 [source], contains an order-form CHSH/Tsirelson theorem and the IsCHSHTuple interface [source]. Physlib’s QuantumInfo.Finite.Pinching constructs the spectral pinching of a state as a completely positive trace-preserving map and proves commutation, fixed-point, Pythagorean, and pinching-bound results [sources]. Lean-Quantum provides basis-independent infrastructure for states, channels, tensor products, Choi and Kraus representations, and trace inequalities [source]; Lean-QIT develops a compositional infrastructure for quantum-information theory [source]. Zhao and Yu formalize CHSH rigidity in Lean 4 [source]. Isabelle/HOL developments cover projective measurement, quantum computation, and the CHSH upper bound [sources]. These developments choose different carriers for states and different bundling conventions, and results proved in one seldom apply verbatim in another. The engineering question underneath is interface design: which objects stay bare predicates, which get bundled, and how finished results are handed to the interfaces a large library expects. We make no priority claim for projective measurement, pinching, or Tsirelson’s inequality.

The library described here packages the side conditions of finite projective measurement into a projection-event API over Mathlib matrices. Its main input is an arbitrary projective partition of the identity. The partition induces two canonical expectations: the pinching, which deletes off-block terms and maps the matrix algebra onto the partition commutant, and the average, which projects further onto the commutative span of the partition. The same event definitions feed the Lüders update and the CHSH adapter. This keeps algebraic identities separate from results that use trace, positivity, or state normalization.

The mathematics is classical: Lüders introduced the selective update rule [sources]; pinching by a family of orthogonal projections is a standard averaging operation in matrix analysis [source] and in quantum information [source]; the bimodule and trace-duality laws proved here are the finite-matrix forms of the defining properties of conditional expectations onto subalgebras [sources]; and the CHSH combination with its quantum bound goes back to Clauser, Horne, Shimony, and Holt [source] and to Tsirelson [source]. The contribution of the library is the checked interface: definitions bundled the way Mathlib expects, exact range and uniqueness theorems for both expectations, and adapters into existing Mathlib results.

Lean declaration identifiers are printed throughout in monospaced type, for example partitionPinchingidem; the underscore is part of the identifier. To locate a declaration, search for the exact printed identifier, after removing only TeX’s protective backslash before each underscore, in the EventAlgebra/*.lean files. In the public repository these files are under Lean/EventAlgebra/. Table tab:modules maps each module name to its subject matter. The top-level EventAlgebra.lean file imports these fifteen modules alongside the wider OPH event-algebra library.

The checked development contributes fifteen pieces:

1. an arbitrary supplied projective partition, independent of a selected state or spectral resolution, with its commutant bundled as a StarSubalgebra and its span bundled with multiplication, star, commutativity, and centrality theorems;

2. partition pinching bundled as a complex LinearMap, with exact range and fixed-point theorems, positivity, unitality, trace preservation, the commutant bimodule law, Hilbert–Schmidt geometry, and map-level uniqueness;

3. an exact random-unitary representation of arbitrary partition pinching as the positive uniform average over all independently signed block reflections, together with a global-sign negative control;

4. an orthogonal-state support countermodel showing that the totalized matrix logarithm returns zero where any support-aware extended relative entropy must return infinity;

5. partition averaging bundled as a complex LinearMap onto the span, with exact range, trace duality, map-level uniqueness, tower laws against the pinching, preservation of partition Born statistics, and a classical-conditioning collapse theorem;

6. a typed nonzero-weight Lüders state update, a support theorem and an unguarded fixed-point characterization that exhibit conditioning as a retraction onto its certainty set, and naturality of the typed update under partition pinching for commutant events;

7. an event-to-observable CHSH client that discharges Mathlib-compatible selfadjointness, involutivity, and cross-commutation hypotheses before applying a complementary norm-form bound;

8. a checked state-expectation bound that converts the norm-form theorem into a state-level CHSH bound;

9. a finite-state Robertson theorem for supplied density matrices and Hermitian observables, with the ordinary-commutator form, a noncommuting saturation control, and a separate zero-variance control;

10. the exact quotient induced by a supplied projective partition: equality after block pinching is equivalent to equality under every commutant trace test, while block pinching and commutative partition averaging both erase cross-sector corners;

11. an exact Tsirelson saturation witness: a declared maximally entangled state and four declared projection events inhabiting a bipartite slot-locality interface of the wider library, whose CHSH expectation equals \(2\sqrt2\) exactly, packaged with the cited upper bounds, together with a record-diagonal delimitation proving the classical bound \(2\) for every diagonal state read against four diagonal observables valued in \([-1,1]\);

12. an ideal static phase-POVM/count-fit structure with conditional tomography, exact diagonal/real-closure blindness, and an explicit synthetic inhabitant proving that the structure does not type source operations, producer receipts, or discharge of the phase-sensitive-effect premise;

13. an exact determination boundary for that structure: a coordinate characterization of the phase-sensitivity clause, run-literal pinning of the state diagonal with one free off-diagonal coordinate, affine dependence of every count frequency on that coordinate, a decidable integer receipt window on the phase counts, and the minimal phase-mass receipt (Section 11.1);

14. a static conformance layer for that structure: taking the committed exact lift as a declared phase-sensitive effect, a deterministic exact-arithmetic calculator, an independent verifier, and a composed Lean arithmetic receipt inhabit the static model with generated expected-frequency numerators satisfying the assumed Born-fit equations, the scaling law, and the integer receipt window (Section 11.2); and

15. a reproducible, version-pinned artifact with per-declaration axiom output, no proof placeholders, and a documented catalog of the Mathlib gaps, scoped-instance hazards, and workarounds met during construction (Section 12).

Two results are outside the current library. No theorem identifies an arbitrary partition with Physlib’s spectral partition. There is no rank-one classical-representation theorem. The CHSH bounds carry a saturation witness (Section 10.2); the witness state and events are declared data, produced by no theorem from any source object. A companion module, Dynamics/ChoiCPTP.lean, defines an explicit finite-matrix CPTP predicate and proves both partition expectations completely positive and trace preserving; the fifteen-module audit here covers their event-algebra interfaces rather than recounting that companion development.

Section 2 fixes the mathematical and Lean interfaces. Sections 3 and 4 treat projection events and selective update. Section 5 gives the bundled partition pinching and its geometry, Section 6 the random-unitary representation and logarithm-support boundary, and Section 7 the averaging expectation, the two-level structure, and the partition-relative operational quotient. Sections 8, 9, and 10 describe the state functional, finite-state uncertainty, and the CHSH clients with the exact saturation witness and its record-diagonal delimitation. Section 11 describes the ideal static phase-POVM/count-fit model, its synthetic non-discharge control, and the declared-effect conformance fixture for the phase-count layer. Section 12 records the Mathlib engagement. Section 13 reports the audit methodology, and Section 14 positions the development feature by feature.

Mathematical and formal setting

Let \(\mathrm{M}_n(\mathbb C)\) be the complex \(n\times n\) matrices, with conjugate transpose \(X\mapsto X^*\), trace \(\operatorname{Tr}\), and identity \(\mathbf 1\). Following the standard finite-dimensional setting [source], a projection event is a Hermitian idempotent \(P=P^*=P^2\), a state is a positive-semidefinite matrix \(\rho\) with \(\operatorname{Tr}(\rho)=1\), and the trace pairing is \(\mu_\rho(M)=\operatorname{Tr}(\rho M)\).

Lean represents these interfaces as predicates over Mathlib matrices: IsEvent P is the conjunction \(P^*=P\) and \(P^2=P\); IsState rho is positive semidefiniteness and unit trace. For functions that return states, the library defines the subtypes ProjectionEvent n and StateMatrix n. The split is practical. Algebraic lemmas use raw matrices. A function advertised as a state update returns a value whose type carries the state conditions.

Table tab:modules lists the fifteen source modules. The comparison in this work concerns their compiled interfaces and uses, not the number of declarations in each file.

Three Mathlib scopes affect compilation. ComplexOrder equips \(\mathbb C\) with the partial order in which \(0\le z\) means that \(z\) is real and nonnegative. MatrixOrder supplies the Loewner order. Matrix.Norms.L2Operator activates the finite-matrix operator norm and C*-ring instances used by the matrix CHSH theorems. Without the right scope, Lean may report an instance problem even though the required theorem is in scope; Section 12 describes the failure modes.

Documentation tags classify results as algebra-only or trace-dependent. These tags do not define an import hierarchy. They record whether a proof uses ring, star, and norm structure alone, or also uses \(\operatorname{Tr}(\rho M)\), positivity, or normalization.

Projection events and the trace pairing

The event layer proves the expected closure rules. Zero, identity, and \(\mathbf 1-P\) are events. Orthogonality is symmetric. Orthogonal sums and products of commuting events are events. Subevent absorption holds on both sides, and every event is positive semidefinite. The declaration IsEvent.onesubtwosmulinvolution proves that \(\mathbf 1-2P\) is a selfadjoint involution. The CHSH adapter in Section 10 uses this result.

The trace pairing is additive, homogeneous, compatible with finite sums, and obeys the sandwich identity \[\operatorname{Tr}(P\rho P)=\operatorname{Tr}(\rho P)\] for idempotent \(P\). Hermiticity of \(\rho\) and \(P\) implies that the pairing is real. Positivity of \(\rho\) and the event property imply \(0\le\mu_\rho(P)\) in Mathlib’s order on \(\mathbb C\); for a state the upper bound is \(\mu_\rho(P)\le 1\). The order-form statements are strictly stronger than their real-part corollaries, and both forms are provided.

The declaration isEventaddandbornWeightaddoforthogonal returns two facts: the orthogonal sum is an event, and its Born weight is the sum of the two Born weights. The event and orthogonality hypotheses carry the first conjunct; the weight identity is linear and uses none of them.

Lüders update as a partial state interface

For raw matrices, the library uses the totalized formula \[\mathcal L_P(\rho)=\mu_\rho(P)^{-1}P\rho P.\] Lean’s field inverse maps zero to zero, so the formula is total and covers algebraic identities in the zero-weight case. Its return type is a raw matrix and carries no state guarantee. The typed operation is \[\begin{aligned} \texttt{luedersStateUpdate}:\quad& \texttt{StateMatrix n}\to\texttt{ProjectionEvent n}\\ &\to(\mu_\rho(P)\ne0)\to\texttt{StateMatrix n}. \end{aligned}\] This operation assumes NeZero n. The unique \(0\times0\) matrix cannot have unit trace, so a state-returning function must exclude that dimension.

The fixed-point theorem needs no nonzero-weight guard. A state fixed by a zero-weight totalized update would equal the zero matrix, which has the wrong trace. The raw function covers the zero-weight case; the state theorem does not carry a redundant premise.

The module assembles these results into a fixed-point description of conditioning. The set certainStates collects the states that assign weight one to \(P\). Conditioning any state of nonzero weight lands in that set in a single step (luedersUpdatememcertainStates), acts on the set as the identity, and, among states, fixes exactly its elements. Conditioning on \(P\) is therefore a retraction of the nonzero-weight states onto its own fixed-point set. The identity case rests on a support theorem, muleqselfofbornWeightone: a state certain of \(P\) absorbs the event on both sides, \(\sigma P=P\sigma=\sigma\). The checked proof compresses \(\sigma\) by the complement event, whose weight vanishes; positive semidefiniteness forces the zero-trace compression to vanish; and the Cauchy–Schwarz property of the state’s quadratic form eliminates \(\sigma(\mathbf 1-P)\) itself.

Bundled arbitrary-partition pinching

A ProjectivePartition n k consists of projections \((P_i)_{i<k}\), pairwise orthogonality, and \(\sum_iP_i=\mathbf 1\). It induces \[\mathcal E_\pi(X)=\sum_iP_iXP_i, \qquad N_\pi=\{X:XP_i=P_iX\text{ for every }i\}.\] The code defines \(N_\pi\) as ProjectivePartition.commutant, a StarSubalgebra defined using Mathlib’s centralizer, and bundles \(\mathcal E_\pi\) as partitionPinchingLinearMap. The membership theorem memcommutantiff reduces membership to the pointwise commutation equation.

The range is a block-diagonal commutant and need not be commutative. For this reason, we do not call it a “classical algebra”; the classical layer is the span of Section 7. The library has no theorem identifying the span with the center of the commutant, and no rank-one classical-representation theorem.

The corresponding declarations are partitionPinchingunital, partitionPinchingposSemidef, tracepartitionPinching, partitionPinchingidem, partitionPinchingeqselfiffmemcommutant, and rangepartitionPinchingLinearMap. State preservation is exposed by partitionPinchingisState.

The corresponding declarations are partitionPinchingbimodule, traceconjTransposepartitionPinchingmul, tracepartitionPinchingpythagoras, tracepartitionPinchingcontraction, tracepartitionPinchingmulcommutant, and partitionPinchingLinearMapunique. Together they make the map a positive, unital, trace-preserving linear projection with a bimodule law and a trace-duality characterization; these are the identities that characterize the trace-preserving conditional expectation onto a subalgebra in the operator-algebra literature [sources]. The library proves the identities directly for this map. This core module does not instantiate an operator-algebra conditional-expectation interface. The companion Dynamics/ChoiCPTP.lean separately proves its custom finite-matrix IsCPTP predicate from the same Kraus and trace identities.

Lüders naturality

If \(P\in N_\pi\), compression commutes with pinching. After normalization, trace preservation against commutant elements gives \[\mathcal E_\pi(\mathcal L_P(\rho))= \mathcal L_P(\mathcal E_\pi(\rho)).\] The raw formula is partitionPinchingluedersUpdate. The theorem partitionPinchingluedersStateUpdate states the same naturality for StateMatrix n and ProjectionEvent n: the input and output are states, and the nonzero-weight proof is transported by bornWeightpartitionPinching. This checks the same operation through the bundled state and event interfaces.

Random-unitary pinching and the entropy support boundary

The support-aware majorization precursor has an exact finite representation. For each sign assignment \(s:\{0,\ldots,k-1\}\to\{\pm1\}\), set \[U_s=\sum_i s(i)P_i .\] Orthogonality and completeness make every \(U_s\) a selfadjoint unitary. The independent sign characters obey \(\sum_s s(i)s(j)=2^k\delta_{ij}\), hence \[\frac1{2^k}\sum_s U_s X U_s^*=\sum_iP_iXP_i=\mathcal E_\pi(X).\] The real weights are strictly positive and sum to one, so this is a literal random-unitary representation. A two-coordinate control proves that replacing the independent sign family by only the global pair \(\{I,-I\}\) leaves an off-diagonal matrix unchanged and is not pinching. These statements are checked in RecordMajorization.lean. They are an algebraic precursor; they do not prove spectral majorization or entropy monotonicity.

The support layer cannot be bypassed by totalizing the logarithm. In Lean, \(\log 0=0\); continuous functional calculus therefore sends the logarithm of every projection to the zero matrix, since a projection’s spectrum lies in \(\{0,1\}\). Consequently the raw finite expression \[\operatorname{Re}\operatorname{Tr}\!\left[\rho(\log\rho-\log\sigma)\right]\] is zero for the two orthogonal rank-one coordinate projections. Both are density matrices, but the first support is not contained in the second. Thus any extended-real divergence that returns \(+\infty\) on support failure cannot equal this totalized raw formula. The density, support, zero-value, and inequivalence receipts are checked in SpectralEntropyBoundary.lean.

This is a fail-closed architectural result, not a no-go for Umegaki entropy. A complete continuation must define the support-aware extended divergence and then prove the pinching relative-entropy Pythagorean identity, spectral majorization, constrained maximum-entropy formula, and the two-level publicization information chain.

Averaging on the partition span

The same partition carries a second canonical expectation. The partition span \[D_\pi=\operatorname{span}\{P_i\}\] is bundled as ProjectivePartition.span. Its closure package is proved by span induction.

Only the inclusion into the center is used here. The reverse inclusion is not part of this module’s API; zero projectors are removed in the separate active-label coordinate equivalence. The averaging map is \[\mathcal A_\pi(X)=\sum_i\frac{\operatorname{Tr}(XP_i)}{\operatorname{Tr}(P_i)}\,P_i,\] bundled as partitionAverageLinearMap. Lean’s zero-totalized inverse makes the terms of zero projectors vanish, so no nonzero-block hypothesis appears anywhere in the module: a zero projector contributes zero to both sides of every identity below.

The corresponding declarations are partitionAverageunital, partitionAverageposSemidef, tracepartitionAverage, partitionAverageidem, partitionAverageeqselfiffmemspan, rangepartitionAverageLinearMap, tracepartitionAveragemulofmem, and partitionAverageLinearMapunique; state preservation is partitionAverageisState. The uniqueness proof mirrors the pinching case: the difference lies in the star-closed span, is trace-orthogonal to its own conjugate transpose, and vanishes by faithfulness of the trace.

The collapse identity is the finite-matrix form of classical conditioning: on the commutative layer, conditioning on an observed partition member replaces the averaged state by the indicator of that member, normalized. The identity is stated for raw matrices; the only hypothesis is the nonzero outcome weight.

The same partition also gives an exact operational quotient. Two matrices \(X\) and \(Y\) are declared equivalent when

\[\operatorname{Tr}(XC)=\operatorname{Tr}(YC) \qquad\text{for every }C\text{ commuting with all }P_i.\]

The theorem is relative to a supplied partition. It neither constructs a physical sector decomposition nor identifies the commutant with a laboratory readout algebra.

For every supplied projective partition, averaging maps surjectively onto the commutative partition-span algebra. It factors through block pinching, and every value commutes with the partition commutant. A one-block rank-two control keeps the maps distinct: pinching retains a within-block coherence which averaging removes. The finite matter interface bundles the same map as a typed public-record adaptor. These statements are machine-checked in B10EdgeCenterAction.lean. The interface adds no edge object, edge-to-partition identification, source selection, or physical detector interpretation to the event-algebra theorems.

The bundled state expectation

For a matrix \(\rho\), stateExpectationLinearMap rho bundles \(M\mapsto\operatorname{Tr}(\rho M)\) as a complex-linear functional. If \(\rho\) is a state it maps identity to one. If \(\rho\) and \(M\) are positive semidefinite, then the expectation is nonnegative. The proof of expectationnonneg uses a finite spectral decomposition of \(M\), cycles the trace, and reduces the result to a sum of products of nonnegative diagonal entries; Section 12 explains why this elementary route was chosen. Additivity and homogeneity come from the bundled LinearMap interface and are not repeated as pointwise lemmas.

Finite-state Robertson uncertainty

Let \(\rho\) be a supplied density matrix and let \(A\) and \(B\) be supplied Hermitian matrices. Write \[A_0=A-\operatorname{Tr}(\rho A)\mathbf 1, \qquad B_0=B-\operatorname{Tr}(\rho B)\mathbf 1,\] and define \[(\Delta_\rho A)^2=\Re\operatorname{Tr}(\rho A_0^2), \qquad c_\rho(A,B)=2\Im\operatorname{Tr}(\rho A_0B_0).\] Hermiticity makes both subtracted expectations real. The positive matrix \(\rho\) induces the seminormed pairing \[\langle X,Y\rangle_\rho=\operatorname{Tr}(Y\rho X^*).\] It may be degenerate when \(\rho\) is not faithful, which is why the formal proof uses Mathlib’s positive-semidefinite matrix seminorm rather than silently assuming a positive-definite state.

The exact two-level control uses \(\rho=|{+z}\rangle\langle{+z}|\). Pauli \(X\) and \(Y\) do not commute, have unit variance, and saturate the bound with \(c_\rho(X,Y)=2\). Pauli \(Z\) and \(X\) also do not commute, while \(Z\) has zero variance and the state commutator readout vanishes. The theorem is an uncertainty statement for supplied finite inputs. It selects no state, observable, Hamiltonian, or physical instrument.

CHSH interoperability as a client

For selfadjoint involutions \(a_0,a_1,b_0,b_1\) with cross commutation, set \[S=a_0b_0+a_0b_1+a_1b_0-a_1b_1.\] The development first proves, in a bare ring, \[S^2=4\mathbf 1-(a_0a_1-a_1a_0)(b_0b_1-b_1b_0)\] (chshmulself). In a nontrivial unital C*-ring this yields the operator-norm bound \(\lVert S\rVert\le2\sqrt2\) (tsirelsonbound), the norm form of Tsirelson’s inequality [source] for the CHSH combination [source]. The analytic half is short: selfadjoint involutions have norm one by the C*-identity (normeqoneofselfAdjointinvolution), commutators of norm-one elements have norm at most two (normcommutatorletwo), and the square identity converts these bounds into \(\lVert S\rVert^2\le8\). The precise Mathlib structure is a NormedRing, StarRing, CStarRing, and Nontrivial. The result is stated for a unital C*-ring.

The theorem tsirelsonboundofisCHSHTuple accepts Mathlib’s IsCHSHTuple. The matrix instantiation, matrixtsirelsonbound, activates Mathlib’s scoped operator norm. The declaration matrixtsirelsonboundofevents accepts four projection events plus the four cross-commutation equations, constructs the dichotomic observables \(\mathbf 1-2P\), and returns the norm bound. This gives the event layer a compiled path into the CHSH theorem.

Mathlib’s tsirelsoninequality is an order inequality in a star-ordered real algebra [source]. The theorems in this artifact are an operator-norm bound, its state-level corollary below, and the exact equality witness of Section 10.2.

The state-level corollary

The bridge from norms to states is the checked bound \[\lvert\operatorname{Tr}(\rho M)\rvert\le\lVert M\rVert\] for every state \(\rho\) and observable \(M\) (normexpectationlel2opNorm). The proof diagonalizes the state, cycles the trace to \(\operatorname{Tr}\!\bigl(D\,(V^*MV)\bigr)\), dominates every diagonal entry of the conjugated observable by the operator norm (normdiagentrylel2opNorm, by testing against a standard basis vector), uses that unitary conjugation does not increase the norm (normeqoneofmemunitaryGroup with submultiplicativity), and sums the nonnegative eigenvalues to one. Composing with the event-level norm bound gives the state-level CHSH corollary (matrixstatetsirelsonboundofevents): for a state and four projection events with cross-party commutation, \[\bigl\lvert\operatorname{Tr}(\rho S)\bigr\rvert\le2\sqrt2\] for the CHSH combination \(S\) of the dichotomic observables \(\mathbf 1-2P\). The pairing \(\operatorname{Tr}(\rho S)\) is real by starbornWeight, since \(S\) is selfadjoint, so the modulus bound is a two-sided real bound. Section 10.2 exhibits a declared witness attaining the bound.

Exact saturation on the slot-locality interface

The module TsirelsonSaturation.lean supplies the attainment witness. Its carrier objects come from the wider library. A supplied bipartite slot split of the record algebra, committed as the interface SlotLocalityInterface, which carries a norm-form Tsirelson bound through the theorem slotlocalityreceipts. The module inhabits that interface at two-dimensional slots with the singleton identity Kraus family (bellSlotInterface). The declared state is the normalized maximally entangled state on the four-dimensional product carrier, transported to \(\mathrm{Fin}\,4\) along a fixed index equivalence so that the typed state and expectation vocabulary of Sections 2 and 8 applies (bellStateisState). The four declared events are the spectral projections of the two Pauli directions on the left slot and of the two quarter-rotated directions on the right slot; each carries a checked event certificate, and the four cross-party commutations are checked on the product carrier.

The equality is chshsaturation; its modulus form is chshsaturationnorm. The packaged statement, tsirelsonsaturationreceipt, is one conjunction over one witness: the committed norm bound of the interface cited at the witness, the state-level bound of Section 10.1 (matrixstatetsirelsonboundofevents) cited at the four events for every state on the carrier, the state certificate with the exact attainment in value and in modulus, and the identification of the attaining observable with the slot-lifted CHSH operator of the interface witness (toFourchshProdeq). The two upper bounds are cited from the committed theorems, not re-proved.

The boundary is declared data. The saturating state and the four events are declarations of the module; no theorem produces them from committed source runs, and no physical regions, spacelike separation, or observer instruments are constructed. Identification of the supplied finite event-order structure with an observer-produced physical spacetime is not supplied, and the receipt consumes the bipartite slot split as a supplied datum.

The record-diagonal classical delimitation

The same module bounds the classical side. For convex weights \(w\) and four diagonal observables \(a_0,a_1,b_0,b_1\) valued in \([-1,1]\) on any finite carrier, the CHSH expectation obeys the classical bound \[\Bigl|\sum_i w_i\, (a_{0i}b_{0i}+a_{0i}b_{1i}+a_{1i}b_{0i}-a_{1i}b_{1i})\Bigr|\le2\] (diagonalchshletwo); the matrix form, for a diagonal state read against four diagonal readouts in the CHSH combination, is diagonalstatechshletwo. In particular, the counted correlation state of the wider library, a record-diagonal state assembled from the counted joint run of the committed observer pair \((86,247)\), obeys the bound \(2\) against every quadruple of diagonal \([-1,1]\)-valued readouts (countedstatediagonalchshletwo). Record-basis diagonality is therefore insufficient for the value \(2\sqrt2\). This is a delimitation of one fixed diagonal state with four readouts diagonal in the same basis, not of arbitrary contextual classical experiments. The Bell state and all four attaining settings are real matrices, so the proved gap is entanglement, non-diagonal coherence, and noncommutativity; it does not isolate the genuinely complex Pauli-\(Y\) direction of the declared phase-sensitive effect, and no theorem asserts that the committed phase lift is necessary or sufficient for attainment.

The delimitation extends from one fixed counted state to the whole committed production surface (SourceReachabilityDelimitation.lean). The module defines the class of states reachable from the three source-counted occupation laws under every operation the development commits: the walk-step transports, the internal slot exchange, the ambient anchorings, the marginalizations, the regional and scalar conditional expectations, marginal products, and convex mixtures. Every state in that class remains diagonal in the record basis with nonnegative weights summing to one, and its CHSH value against any four record-diagonal \([-1,1]\)-valued readouts is at most \(2\), strictly below the attained \(2\sqrt2\) of the declared witness. The witness state itself carries an off-diagonal entry of one half, so no map that preserves record diagonality reaches that particular witness from the class. This target-specific obstruction does not show that every realization of the value \(2\sqrt2\) requires non-diagonal preparation: readouts that are not slot-local with respect to the declared split are outside the bound, and the slot-local separability theorem for arbitrary settings is supplied by the companion module described next. The result is a statement about the committed operation class and the declared Bell-state witness; every conceivable architecture extension is outside its scope. Like Dynamics/ChoiCPTP.lean, the module is a companion in the wider library, outside this paper’s fifteen-module count and scale table.

The companion module ProductSplitSeparability.lean lifts the jointly-diagonal restriction on the declared slot split. A product-basis diagonal state with a probability diagonal is the explicit convex combination of the point states \(e_{aa}\otimes e_{bb}\) weighted by its diagonal entries (productDiagonalseparable), and against any four Hermitian settings in the Loewner unit interval, two on each slot and with no commutation assumed inside a slot, its slot-local CHSH trace is real with modulus at most \(2\) (productDiagonalslotLocalchshletwo). Every reachable state on the two committed pair carriers is therefore separable across the split and obeys the bound against all slot-local unit-interval readouts. Slot membership is the hypothesis that carries the bound: the Bell settings conjugated by \(\mathrm{CNOT}\,(H\otimes1)\) commute pairwise across the wings, lie in the unit interval, and reach exactly \(2\sqrt2\) on the product-diagonal state \(|00\rangle\langle00|\), with one of them in neither slot (crossWingcommutationnotsufficient). A slot-local value above \(2\) on a state certifies off-diagonal record coherence; the theorem supplies neither physical regions nor a source preparation. Like the reachability module, it is a companion in the wider library, outside the fifteen-module count and scale table.

An ideal static phase-POVM count fit

The module OperationalPhaseInstrument.lean makes the interface boundary machine-visible. Its structure IdealPhasePOVMCountModel is an ideal static model: one matrix state, the committed web effects plus one designated phase effect, exact binary POVM certificates, integer count literals with the diagonal pair fixed to \((111,68)\), and exact frequency-equals-Born equations. It contains no source operation, completely-positive outcome maps, trace-preserving summed channel, postmeasurement state, readback implementation, producer identity, receipt binding, or statistical validation rule.

Every ideal model yields fixed-trace identification (idealphasemodelcompletestomography), and its state is the unique state fitting all exact equations (preparationidentifiedbyexactfitdata). The construction modelOfIdealPhaseFitData is equivalent only to the existence of IdealPhaseFitData (hasIdealPhaseFitiffdata); this is an algebraic fit statement rather than a theorem establishing the phase-sensitive effect.

Two incompleteness controls are exact. Two certified distinct states carry identical Born data on every diagonal effect (diagonalcontextinsufficient), so the diagonal context alone identifies no state; the committed rotated context separates that pair; and no diagonal effect and no complexified real effect satisfies the phase-sensitivity clause (phaseeffectnotdiagonal, phaseeffectgenuinelycomplex). Hence a complete static family needs non-diagonal content and some separator outside the complexified-real closure (phasecontextnecessary). The theorem does not force the particular rotated effect, the designated phase effect, their order, or an operational implementation.

The non-discharge boundary is exact. The declaration syntheticIdealPhaseFitData chooses the rational diagonal state with weights \(111/179\) and \(68/179\), rotated counts \((315,401)\), and phase counts \((1,1)\). The theorem syntheticidealphasefit proves that these chosen literals inhabit HasIdealPhaseFit without any producer, run, operation, or receipt input. Exact finite frequency equality is also not a general validation criterion for sampled data. Therefore ideal fit cannot certify custody or establish the phase-sensitive effect. A genuine target needs source-attached CP outcome maps, a trace-preserving summed channel, operation/readback and common-preparation semantics, producer-bound receipts, and a preregistered statistical validation rule (or an explicitly exhaustive deterministic semantics). Operational additivity and composition require a separate cross-context additivity premise.

Exact determination boundary and the integer receipt window

The module PhaseInstrumentDetermination.lean sharpens the boundary to an exact reduction. The phase-sensitivity clause has a coordinate characterization: for a Hermitian effect \(E\) the Born-weight gap between the two Pauli-Y states equals \(-2\,\mathrm{Im}\,E_{01}\) (bornWeightrhoYsubofisHermitian), so the clause holds exactly when \(\mathrm{Im}\,E_{01} \neq 0\) (phasesensitivityiffoffdiagim). The diagonal and complexified-real exclusions are the \(\mathrm{Im}\,E_{01} = 0\) instances, and conjugating a committed web projector by any real matrix, gauge images and permutations included, is excluded in one statement (phaseeffectnerealconjugatedweb).

The committed run literals pin the model state. Every inhabitant satisfies \(\rho_{00} = 111/179\), \(\rho_{11} = 68/179\), and \(\rho_{10} = \overline{\rho_{01}}\) (prepcoordinates), so one complex off-diagonal coordinate carries the entire remaining state content. Every count frequency of every inhabitant, in every instrument context, is an exact affine function of that coordinate, with real coefficients determined by the context’s effect entries (frequencyaffine). Over the committed core the phase frequency equals \(1/2 - \mathrm{Im}\,\rho_{01}\) (phasefrequencyeq) and the rotated frequency equals \(315/716 - (\sqrt{3}/2)\,\mathrm{Re}\,\rho_{01}\) (rotatedfrequencyeq); two committed-core inhabitants have equal states exactly when all count frequencies agree (prepeqifffrequencieseq). Positivity bounds the coordinate by \(|\rho_{01}|^2 \le 7548/32041\) (prepoffdiagnormSqle), which forces the decidable integer window \(32041\,(a-b)^2 \le 30192\,(a+b)^2\) on the phase counts \((a,b)\) of every committed-core inhabitant (phasecountsreceiptwindow). Both phase outcomes of every committed-core inhabitant carry positive mass, and the minimal phase count mass over committed-core inhabitants is exactly two, attained by the synthetic inhabitant (minimalphasecountmass).

The reduction states the phase residue exactly: for a committed-core inhabitant the state diagonal, the affine dependence of every count frequency on the one free coordinate, and the admissible count window are forced by the committed diagonal literals and the committed effects. Two operational requirements are not encoded by this static type: a representation of the measurement by completely positive outcome maps with a trace-preserving summed channel and compatible effects, and a source-produced common preparation that selects the context and produces the public outcomes. The window is a necessary arithmetic condition only and carries no provenance information, since the synthetic inhabitant meets it without a source run.

Static conformance fixture for the phase-effect layer

The committed exact lift \(I/2 - (2\sqrt{3}/3)\,i\,(QP - PQ)\), equal to the Pauli \(+Y\) projector, is taken as a declared phase-sensitive effect. It is not a state transition or an instrument. The module consumes that declaration and inhabits IdealPhasePOVMCountModel over the committed core with static integer literals. A deterministic calculator expands the Born table of the declared effects on the declared matrix \(\mathrm{diag}(111/179, 68/179)\) in exact arithmetic over \(\mathbb{Q}(\sqrt{3}, i)\): each context pair is the exact Born weight of the context effect scaled to the least positive integer multiple of the reference mass \(179\) clearing its denominator, giving \((111, 68)\) at mass \(179\) in the diagonal and record-conjugate contexts, \((315, 401)\) at mass \(716\) in the rotated contexts, and \((179, 179)\) at mass \(358\) in the phase context. These are generated expected-frequency numerators, not observations or validation. No sampling or floating-point step occurs. An independent verifier sharing no arithmetic code rebuilds the table from the pinned payload and demands exact agreement with every receipt field, run-mass-multiple minimality and the integer window included. The composed receipt (operationalPhaseAttainmentreceipt) derives, from one antecedent bundle pinned to the declared effect and matrix, the conjunction: committed core, declared effect in the phase slot, vanishing off-diagonal matrix entry, committed diagonal literals, the stored Born-fit equations and their cross-multiplied scaling consequences, positive integer masses, and phase counts inside the registered window. The Lean theorem does not prove leastness, source reachability of this two-dimensional matrix, or receipt provenance; the external verifier checks the deterministic least-denominator arithmetic separately. The instrument representation, the source-produced preparation, and the independent cross-context additivity premise are not supplied.

The module LuedersPhaseInstrument types the channel clauses as a structure PhaseInstrument on the eight committed contexts: outcome maps that are completely positive, trace-nonincreasing on positive-semidefinite inputs, summing to a trace-preserving channel per context, and inducing the committed effect table. The Lüders maps \(X \mapsto EXE\) inhabit it (luedersPhaseInstrument) with a singleton Kraus family, and the normalized post-measurement state is certain of its effect (luedersPhaseInstrumentrepeatable). On \(\mathrm{diag}(111/179, 68/179)\) the outcome traces reproduce the fixture frequencies, with \(1/2\) in the phase context, whose post-measurement state is the declared \(+Y\) projector itself; the phase and diagonal values are also obtained by direct matrix computation through the outcome maps, with no use of the stored Born-fit equations. A swap-twisted instrument meets every channel clause with the same induced effects, differs on the record entry, and fails repeatability (effecttabledoesnotdetermineinstrument). Certain-state invariance does select it: a Kraus-form outcome map with projective induced effect \(E\) that leaves every state certain of \(E\) unchanged is the Lüders map \(X \mapsto EXE\), and conversely, so among Kraus-form instruments with the committed effects the Lüders instrument is exactly the certain-state-invariant one; the swap-twisted instrument fails that invariance, and the committed repeatability clause (the normalized output is certain of its effect) is strictly weaker and does not select (InstrumentSelectionByCertainStates). Certain-state invariance is a declared operational hypothesis, no source implements it, and the instrument representation, the source-produced preparation, and cross-context additivity are not supplied. The module is a companion in the wider library, outside the fifteen-module count and scale table.

The companion module SourcePhaseSelection asks what phase-sensitive effect candidates can be built from source-attached algebraic fields. Its generator reads two inputs only, the six exact rows of the declared two-dimensional irreducible representation and the diagonal record projector, forms the projector orbit, and enumerates the twelve noncommuting orbit pairs. A declared complexification adapter sends each nonzero real skew commutator \(C\) to \(I/2-iC/(2|C_{01}|)\). The generated effect values are exactly the two Pauli-\(Y\) projectors (generatedeffectvaluesexact); the first pair in the current stable label order has the \(+Y\) projector, which equals the declared lift and the instrument’s phase slot (currentfirstlabelledeffecteqsourcePhaseLift, currentfirstlabelledeffecteqdeclaredluederseffect). Eight pairs give \(+Y\) and four give \(-Y\), so the theorem is effect-value equality rather than witness uniqueness. Reversing the commutator order for a fixed pair swaps the transpose effects (effectMatrixnegativeeqtransposepositive), but reversing the event list does not generally flip the conventional first-labelled orientation: the last current pair is also \(+Y\). No theorem source-selects the first-label rule. The robust result is the unordered pair of \(Y\) projectors under the declared adapter. The module’s enabled-domain relation reproduces the canonical \(36/12\) split between state-changing Lüders updates and equality stutters (changingEnabledCellCensus, alreadyOperationEnabledCellCensus). It constructs no instrument and supplies no preparation, outcome, readback, or provenance; the phase-sensitive-effect declaration keeps the adapter and orientation choice. Like the reachability module, it is a companion in the wider library, outside the fifteen-module count and scale table.

The companion module SourcePhaseInstrumentOutcomeBridge joins those generated source semantics to the declared Lüders phase instrument. It maps every generated \(+Y\) event to the declared phase-outcome index \(0\) and every generated \(-Y\) event to index \(1\), then proves exact equality of the generated effect with that entry of the committed effect pair (generatedEffecteqcommittedPhaseOutcome). All five generated state matrices are positive semidefinite with trace one (stateMatrixisState). For each of the 48 enabled source steps the corresponding Born weight is nonzero, and the normalized output of the indexed declared Lüders map equals the generated semantic result matrix (sourceStepnormalizedluedersoutcomeeqresult). This is a matrix-level compatibility theorem. The index is not a recorded public outcome, and the result neither source-selects nor implements the Lüders instrument, nor supplies one common cross-context preparation, readback, run binding, provenance, or custody. The clauses are conjoined in sourcePhaseInstrumentOutcomeBridgereceipt.

The companion module SourcePhaseCommonPreparationHull identifies the exact common-support surface of the generated phase relation. Exactly the three real orbit states admit all twelve generated phase events (hasAllPhaseEventsiff). Their normalized real mixture with weights \[\frac{265}{537},\qquad \frac{136}{537},\qquad \frac{136}{537}\] is exactly the declared run state; this is theorem commonSupportMixtureeqcommittedRunState. Equality to that matrix uniquely determines all three coefficients, without assuming normalization (commonSupportMixturecoefficientsunique). Each common-support state assigns weight \(1/2\) to either generated Pauli-\(Y\) orientation, and every common-support state/event pair inherits the normalized declared Lüders-outcome equality. The declared run matrix is not any generated state, no generated source step starts from it, and the result of every generated phase event lacks all-event support. This is retrospective convex-hull compatibility, not a source-produced or enabled common preparation. The pointwise one-step cells supply no convex-lift, mixing, reset, re-preparation, or sequential schedule. The twelve generated events are not the eight public instrument contexts, and the theorem supplies no instrument implementation, public outcome, readback, run binding, provenance, custody, cross-context additivity, or physical attachment. The clauses are conjoined in sourcePhaseCommonPreparationHullreceipt.

The module SourcePhaseBornWeightBoundary proves the exact single-shot identity \[\operatorname{Tr}(\rho P_{+Y})=\frac12-\operatorname{Im}(\rho_{01})\] for every normalized two-dimensional state. Thus a non-half weight for the current conventional first-labelled \(+Y\) effect under the declared adapter/order weight requires nonzero imaginary off-diagonal coherence; real off-diagonal coherence alone is insufficient (statecurrentfirstlabelledweighteqhalfsubim). It then places that conventional effect and the enumerated source-reachable class behind an explicit prospective preparation-bridge interface. If such a bridge maps reachable matrices to states and preserves record diagonality, the selected \(+Y\) effect has Born weight exactly \(1/2\) on every bridged preparation (reachablerecordPreservingphaseweighthalf). On a record-diagonal state the generated \(-Y\) orientation and the diagonal comparator \((1/2)I\) have the same weight. Constant diagonal and off-diagonal bridges show that the preservation hypothesis is logically inhabitable and load-bearing. Both are mathematical controls that ignore their inputs. The result derives no source bridge or operation, common preparation, public outcome, sequential instrument behavior, operational readback, run, provenance, or custody.

Working over Mathlib: scopes, gaps, and affordances

This section records what the construction consumed from Mathlib, where the library resisted, and which workarounds closed the gaps. The artifact repeats the catalog in the notes file MATHLIBNOTES.md.

Scoped instances

The three scopes of Section 2 share a failure mode. The partial order on \(\mathbb C\) and the Loewner order are scoped instances; every \(0\le z\) goal and every positive-semidefiniteness statement over \(\mathbb C\) elaborates only when the scope is open, and a missing scope surfaces as an instance-resolution error far from its cause. ComplexOrder also carries the scoped ordered-ring structure on \(\mathbb C\) that supplies multiplicativity of nonnegativity inside the complex order. There is no global norm on Mathlib matrices; the operator norm, the NormedRing structure, and the CStarRing instance arrive only under Matrix.Norms.L2Operator, so the entire Tsirelson section lives behind that scope. The Nontrivial instance for \(n\times n\) complex matrices with \(n\ne0\) did not synthesize and is constructed by hand, entrywise. The matrix unitary group is a submonoid distinct from Mathlib’s unitary bundle, so its norm-one property is also proved by hand from the C*-identity.

Gaps and workarounds

Bilinear trace positivity. Mathlib proves \(0\le\operatorname{Tr}(A)\) for a single positive-semidefinite matrix and covers sandwich forms \(BAB^*\). The bilinear statement \(0\le\operatorname{Tr}(AB)\) for two positive-semidefinite factors is absent. For Born weights the gap costs nothing, because \(\operatorname{Tr}(\rho P)=\operatorname{Tr}(P\rho P)\) for idempotent \(P\). For expectationnonneg the natural route, the C*-order equivalence between nonnegativity and Gram factorization, fails to elaborate: two continuous-functional-calculus instances are not synthesized for the matrix algebra under its product topology. The proof takes the elementary route instead, a spectral decomposition of the observable followed by a trace cycle and termwise nonnegativity, in about a dozen lines.

The ring identity. The square identity behind the Tsirelson bound is pure noncommutative ring algebra under side relations: four involutivity equations and four cross commutations. Lean has no noncommutative analogue of linearcombination, and noncommring does not use hypotheses. The checked proof builds a small confluent rewrite system. Each commutation hypothesis is recast as a universally quantified, association-compatible form \(b(ax)=a(bx)\), and each involution as \(a(ax)=x\); applied through simp only, these rules move every \(b\) past every \(a\) in right-associated words and cancel adjacent equal letters. Every rewrite strictly decreases the number of letter pairs out of normal order, so the system terminates, and abel closes the remaining additive goal.

Higher-order motives. Two steps needed their motives spelled out. The binary span-induction principle behind the closure package of Proposition 2 does not infer its motive from the goal; the predicate is passed explicitly. Rewriting with the unit-trace equation inside a hypothesis whose proof term mentions the bundled state predicate fails the motive typecheck, because the state predicate itself contains the trace being abstracted; a term-level chain through injectivity of the real embedding replaces the rewrite.

Rewriting discipline. Unfolding the definition of the Born weight rewrites the first syntactic occurrence, which in normalized expressions is often the normalizing scalar \(\mu_\rho(P)^{-1}\) instead of the intended trace argument. The affected proofs isolate each trace identity as a standalone step with explicit arguments to the trace commutation and cycling lemmas.

Affordances

The Matrix.PosSemidef API is complete enough that the development never unfolds the definition of positive semidefiniteness: sandwich closure, sums, scalar multiples, diagonal nonnegativity, trace nonnegativity, and the Gram construction cover every need, and the scalar lemma accepts a complex scalar that is nonnegative in the complex order, which makes the Lüders normalization a single application. Trace faithfulness is available in two forms: the conjugate-transpose criterion powers the uniqueness theorems of both expectations, and the zero-trace criterion together with the Cauchy–Schwarz property of positive matrices powers the support theorem of Section 4. On the analytic side, the C*-identity, the norm-one property of the unit, and submultiplicativity reduce the norm half of the Tsirelson bound to about forty lines over the four-typeclass signature, and the matrix case is a two-line instantiation behind the norm scope. The state-expectation bound of Section 10.1 rests on the scoped norm being definitionally the Euclidean operator norm: the type synonym is identity-transparent, so a show converts Euclidean-space statements to raw matrix-vector algebra, and the basis-vector, submultiplicativity, and eigenvalue-trace lemmas finish the proof in about sixty lines. Mathlib’s CHSH file supplied the IsCHSHTuple bundle, so interoperability with the order-form theorem cost one conversion theorem.

Artifact evaluation and proof audit

The source is a Lake project. Its toolchain pins leanprover/lean4:v4.29.1; its manifest pins Mathlib commit 5e932f97dd25535344f80f9dd8da3aab83df0fe6. Build the library with

The canonical Lean modules are publicly available in the Observer Patch Holography repository [source]. The exact source snapshot is the repository revision containing this manuscript and its built PDF; the manuscript source accompanies the submission.

Table 1 describes the fifteen modules discussed here and the umbrella root. Other modules imported by the broader root are outside this paper’s count. The comparison in Section 14 concerns interfaces, not counts.

Every public result discussed in the paper appears under its Lean name. The modules end with #print axioms commands for the principal declarations, and a clean build emits the generated output. The 277 audited declarations report only subsets of propositional extensionality, classical choice, and quotient soundness, the standard Lean/Mathlib base. No declaration reports sorryAx, and a source scan finds no sorry placeholder in these modules.

The submitted API uses every orthogonality hypothesis in its orthogonal-sum theorem. The sequential-update theorem has no unused event premise. State update is typed and excludes dimension zero. The fixed-point equivalence has no nonzero-weight guard, and the averaging module carries no nonzero-block hypotheses. The commutant, span, and both expectations are bundled, and the CHSH adapters are clients of the event definitions.

The repository contains the toolchain, Lake manifest, source modules, build command, in-source axiom queries, and a Creative Commons BY-NC-SA 4.0 license. No persistent archive identifier is claimed.

Feature-level comparison

Table tab:comparison compares compiled features. It does not treat a count of elementary lemmas as a research contribution.

Physlib provides more channel structure: its spectral pinching is a CPTPMap [source]. This artifact accepts a supplied partition that need not come from the spectrum of a state. The two APIs therefore have different inputs, and no correspondence theorem connects them.

Lean-Quantum and Lean-QIT cover a larger part of quantum information [sources]. Here, the scope is limited to connections among projections, commutants, spans, the two expectations, selective update, and Mathlib’s CHSH interface.

Limitations and conclusion

The library connects projection events, Born weights, a typed Lüders update, arbitrary projective partitions, the two expectations of a partition, and event-level CHSH bounds in norm and state form, with an exact saturation witness and a record-diagonal classical delimitation on the same event API. The pinching has the bundled commutant as its exact range and the average has the bundled span; each map is the unique trace-dual projection onto its range, the two compose as a tower, and both interact with Lüders conditioning by checked theorems. The supplied-state Robertson bound, the independent-sign representation, the logarithm-support boundary, and the partition-relative operational quotient use the same finite matrix API. Each formal statement in the paper points to a declaration in the repository source.

The construction follows one pattern: state algebraic content as predicates over raw matrices, move to subtypes exactly where an API promises a state, bundle the carrier and the projection so that range and uniqueness theorems are exact, and hand finished objects to Mathlib interfaces through small adapters. The pattern is independent of measurement theory and applies to other finite-dimensional operator-algebra developments over Mathlib.

The companion Dynamics/ChoiCPTP.lean establishes complete positivity and trace preservation for both expectations under a custom finite-matrix IsCPTP interface. There is no theorem connecting the supplied partition to Physlib’s spectral pinching and no rank-one classical specialization. The CHSH saturation witness rests on declared data: no theorem produces the state or the events from a committed source run. The ideal static phase-fit model has an explicit synthetic inhabitant and is not an operational instrument. The entire development is finite-dimensional and says nothing about normal maps on infinite-dimensional von Neumann algebras.

The proved surface contains the arbitrary-partition pinching with its exact range and bimodule law, the averaging expectation with its tower and classical-conditioning laws, typed Lüders naturality, the complete partition-relative quotient, the supplied-state Robertson inequality, the state-level CHSH corollary, the exact saturation receipt with its record-diagonal delimitation, and the ideal phase-fit model with its synthetic non-discharge counterreceipt; the companion module adds the custom CPTP proofs. It contains no Physlib spectral-partition correspondence and no source-selected quantum instrument; the two-qubit saturation witness consists of declared data, and the operational phase instrument and its source custody are not constructed.

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, designed the study, reviewed the formal development, and takes responsibility for the manuscript and artifact.

Data and code availability. No empirical data were generated. The canonical Lean source is available in the Observer Patch Holography repository [source]. The repository revision containing this manuscript provides the Lean source, pinned dependency files, build instructions, and declaration-level axiom queries under a Creative Commons BY-NC-SA 4.0 license. No persistent archive identifier is claimed.

AI Assistance Disclosure

This research project used research-grade commercial models, including Anthropic’s Fable and OpenAI’s GPT-5.6-Sol, for research support, software development, editing, and synthesis. The authors are responsible for the paper’s claims, methods, and final text.