Section 5 — Making measurements projective: definitions #
Definitions for Naimark dilation and orthonormalization, matching
Section 5 of references/ldt-paper/orthonormalization.tex and
Chapter 4 of the blueprint (blueprint/src/chapter/ch04_projective.tex).
Naimark dilation structure #
The key mathematical content is the Naimark dilation theorem: given submeasurements on a bipartite space, there exist auxiliary registers and projective measurements on the enlarged space that preserve all correlations exactly.
One-measurement Naimark (Lemma 5.2) #
The building block is the one-measurement Naimark lemma. Given a
submeasurement {M_a}_{a ∈ α} on Op d, it produces a projective
submeasurement on the enlarged space Op (d × Option α). The auxiliary
register has dimension |α| + 1, with the extra dimension absorbing the
"missing mass" I − ∑ M_a. The construction uses the isometry
V|ψ⟩ = ∑_a √M_a |ψ⟩ ⊗ |a⟩ + √(I−M)|ψ⟩ ⊗ |⊥⟩ and defines
P̂_a = V† (I ⊗ |a⟩⟨a|) V.
Questionwise Naimark data #
For a prospective full bipartite assembly, one-measurement Naimark is applied independently to each question on each side. The current formal interface records these questionwise local data and their marginal preservation identities, not the full tensor-product correlation theorem.
Matrix-level witnesses #
Concrete Matrix d d ℂ witnesses are provided alongside the abstract
operator-algebra formulation, giving honest probability and overlap formulas.
Finite Hilbert space infrastructure #
A finite-dimensional Hilbert space represented by a finite index type.
- carrier : Type u_1
- instDecidableEq : DecidableEq self.carrier
Instances For
Concrete operators on a finite Hilbert space.
Equations
Instances For
The SDP separation argument uses the elementwise finite-matrix norm. These instances record that choice once for the project's concrete operator type, rather than reintroducing it in each analytic argument.
A positive operator used as a possibly unnormalized state witness.
- matrix : MatrixOperator H
Instances For
Concrete submeasurements on a finite Hilbert space.
Equations
Instances For
Concrete measurements on a finite Hilbert space.
Equations
Instances For
View a concrete matrix submeasurement as the paper-local submeasurement structure.
Equations
Instances For
View a concrete matrix measurement as the paper-local measurement structure.
Equations
- M.toMeasurement = { toSubMeas := MIPStarRE.LDT.MakingMeasurementsProjective.MatrixSubmeasurement.toSubMeas M.toSubmeasurement, total_eq_one := ⋯ }
Instances For
The concrete expectation τ(ρ X) on the local matrix layer.
Equations
Instances For
One-measurement Naimark dilation (Lemma 5.2) #
The one-measurement Naimark dilation is the building block for the full
theorem. Given a submeasurement M on space d, it produces a projective
submeasurement on the enlarged space d × Option α, where Option α
models the auxiliary register with one extra dimension none = ⊥ for the
missing mass I − ∑ M_a.
The auxiliary pure-state projector |⊥⟩⟨⊥| on Option α, where ⊥ = none.
This is the initial state of the auxiliary register before the Naimark
isometry is applied.
Equations
Instances For
The lifted density matrix for one-measurement Naimark dilation:
ρ_lifted = |Option α| · (ρ ⊗ |⊥⟩⟨⊥|).
The scaling by |Option α| ensures the normalized trace is preserved:
τ'(ρ_lifted) = τ(ρ), where τ' is the normalized trace on the enlarged space.
Equations
Instances For
One-measurement Naimark dilation data at the matrix level.
Given a submeasurement M : Submeasurement α d, this witnesses the existence
of a projective submeasurement on the enlarged space d × Option α that
preserves all expectation values. This is Lemma 5.2 of the paper.
The construction: let V : H → H ⊗ ℂ^{|α|+1} be the isometry
V|ψ⟩ = ∑_a √M_a |ψ⟩ ⊗ |a⟩ + √(I−M)|ψ⟩ ⊗ |⊥⟩.
Then P̂_a = V† (I ⊗ |a⟩⟨a|) V is a projection, and
⟨ψ|M_a|ψ⟩ = ⟨ψ⊗⊥|P̂_a|ψ⊗⊥⟩.
- source : Quantum.Submeasurement α d
The source submeasurement being dilated.
- liftedEffect : Option α → Quantum.Op (d × Option α)
The dilated projective effects on
d × Option α. For outcomesome a, this is the Naimark projectorP̂_a. For outcomenone, this is the projector for the "missing mass". - lifted_isProj (a : Option α) : Quantum.IsProj (self.liftedEffect a)
Each lifted effect is a genuine orthogonal projection. Positivity follows from
IsStarProjection.nonneg. The lifted projections sum to at most identity (which together with
lifted_isProjimplies mutual orthogonality).- expectation_preservation (ρ : Quantum.Op d) (a : α) : Quantum.normalizedTrace (ρ * self.source.effect a) = Quantum.normalizedTrace (oneMeasLiftedDensity α ρ * self.liftedEffect (some a))
Expectation preservation: for any operator
ρonOp d, the expectation of outcomeaunder the original submeasurement equals the expectation under the dilated projective submeasurement with the Naimark-lifted state. The identity is linear, so it holds for all operators, not just density matrices. This is the core content of the dilation.
Instances For
Positivity of a lifted Naimark effect, derived from its projectivity.
Lean-only consequence of the one-measurement Naimark data: the paper records
the lifted effects as projections, and positivity is supplied here by the
Mathlib star-projection order theorem through IsStarProjection.nonneg.
Questionwise Naimark data #
The current Lean data applies one-measurement Naimark independently to each question on each side.
Questionwise Naimark data for the prospective full assembly.
Given submeasurements on space ι, this carries the questionwise
one-measurement Naimark dilations used as the local building blocks for the
full tensor-product assembly.
- left (x : QuestionA) : OneMeasNaimarkData OutcomeA ι
Alice's questionwise one-measurement Naimark dilations.
- right (y : QuestionB) : OneMeasNaimarkData OutcomeB ι
Bob's questionwise one-measurement Naimark dilations.
Instances For
Error functions for orthonormalization #
The explicit error in thm:orthonormalization.
Equations
Instances For
Error bound of the direct completion-route orthonormalization theorem.
The paper proves the sharper orthonormalizationError ζ. The direct completion
route first converts the completed measurement's 2ζ self-consistency estimate
into a 4ζ source-almost-projective estimate, and therefore uses this weaker
named envelope.
Equations
Instances For
The explicit error in the measurement version of the lemma.
Equations
Instances For
The almost-projective error extracted from a consistency hypothesis.
Instances For
The spectral-truncation error when rounding one almost-projective effect to a
projection via eigenvalue truncation. Dominated by √ζ.
Equations
Instances For
The rounding error when converting an almost-projective POVM to a projective submeasurement.