Section 5 — Statements #
Statements for Naimark dilation, one-measurement Naimark, the orthogonalization lemma, rounding to projectors, rank reduction, and completing to measurement.
Naimark dilation statements #
The one-measurement Naimark lemma (OneMeasNaimarkLemma) is the
building block: any submeasurement can be dilated to a projective
submeasurement on a space enlarged by one auxiliary register.
The questionwise Naimark interface (NaimarkStatement) records the
per-question one-measurement dilations and their single-outcome marginal
preservation identities. It is not the full tensor-product statement of
\label{thm:naimark}.
The source theorem form is recorded separately as
NaimarkTensorProductCorrelationStatement and
naimarkTensorProductCorrelation. This statement contains the full
bipartite auxiliary-state and correlation-preservation conclusion of
\label{thm:naimark} in the projective-submeasurement form supplied by the
paper's one-measurement helper. The proof is the tensor-product assembly
implemented in NaimarkFull.lean.
One-measurement Naimark statement #
Statement of the one-measurement Naimark lemma (Lemma 5.2).
For any submeasurement M on Op d, there exists a one-measurement
Naimark dilation on the enlarged space Op (d × Option α).
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.OneMeasNaimarkLemma α d M = ∃ (data : MIPStarRE.LDT.MakingMeasurementsProjective.OneMeasNaimarkData α d), data.source = M
Instances For
Questionwise Naimark interface #
Paper origin: Lean-only questionwise interface below
docs/paper-gaps/naimark-dilation.tex.
The paper's full tensor-product Naimark dilation
(references/ldt-paper/orthonormalization.tex:36-115,
\label{thm:naimark}) is formalized separately by
NaimarkTensorProductCorrelationStatement. This structure records the
per-question one-measurement dilations of
\label{lem:naimark-helper}
(references/ldt-paper/orthonormalization.tex:121-159) together with the
single-outcome marginal-preservation conclusions used by downstream
projectivization arguments.
This records the questionwise one-measurement Naimark dilations that appear in
the proof of the full theorem: each A x and B y is equipped with a local
projective dilation preserving all single-outcome expectations. The
tensor-product assembly of the paper theorem is the separate source-facing
theorem naimarkTensorProductCorrelation.
Alice's local dilations are attached to the correct source submeasurements.
Bob's local dilations are attached to the correct source submeasurements.
- leftMarginalPreservation (x : QuestionA) (ρ : Quantum.Op ι) (a : OutcomeA) : Quantum.normalizedTrace (ρ * (A x).outcome a) = Quantum.normalizedTrace (oneMeasLiftedDensity OutcomeA ρ * (data.left x).liftedEffect (some a))
Alice's single-outcome expectations are preserved by each local dilation.
- rightMarginalPreservation (y : QuestionB) (ρ : Quantum.Op ι) (b : OutcomeB) : Quantum.normalizedTrace (ρ * (B y).outcome b) = Quantum.normalizedTrace (oneMeasLiftedDensity OutcomeB ρ * (data.right y).liftedEffect (some b))
Bob's single-outcome expectations are preserved by each local dilation.
Instances For
Tensor-product Naimark source theorem #
The density matrix of ψ ⊗ aux, written in the register order used by the
paper's dilated measurements:
(Alice × AliceAux) × (Bob × BobAux).
The source paper writes the dilated vector as
\ket{\widehat{\psi}} = \ket{\psi} \otimes \ket{\mathsf{aux}}. Since the
local dilated measurements act on Alice × AliceAux and Bob × BobAux, the
matrix entries below are the corresponding tensor-product density after the
canonical reassociation and permutation of the four finite registers.
Equations
Instances For
The canonical register permutation from
(Alice × Bob) × (AliceAux × BobAux) to
(Alice × AliceAux) × (Bob × BobAux).
Equations
- MIPStarRE.LDT.MakingMeasurementsProjective.naimarkProductExtensionEquiv HA HB HauxA HauxB = Equiv.prodProdProdComm HA.carrier HB.carrier HauxA.carrier HauxB.carrier
Instances For
The product-extension density is the ordinary tensor-product density after the register permutation used by the dilated measurements.
The product-extension density is positive semidefinite.
The quantum state ψ ⊗ aux in the register order used by the full Naimark
correlation theorem.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product-extension state is normalized whenever both tensor factors are normalized.
Witness data for the full tensor-product Naimark correlation theorem.
Paper origin: references/ldt-paper/orthonormalization.tex:36-80
(\label{thm:naimark}), with the tensor-product assembly proof at
references/ldt-paper/orthonormalization.tex:161-187.
The data records the auxiliary Hilbert spaces, an auxiliary product state, the
dilated state ψ ⊗ aux, and projective submeasurements on the enlarged Alice
and Bob spaces. This is the form produced by
references/ldt-paper/orthonormalization.tex:121-187: the fresh ⊥ outcome
carries the residual mass, so the original outcome family is projective but not
complete in general. The final field is the source theorem's correlation
identity for all questions and original outcomes.
- auxState : QuantumState (HauxA.carrier × HauxB.carrier)
The auxiliary state on the tensor product of the two auxiliary spaces.
- auxState_normalized : self.auxState.IsNormalized
The auxiliary state is normalized.
- auxLeft : QuantumState HauxA.carrier
Alice's factor in the auxiliary product state.
- auxRight : QuantumState HauxB.carrier
Bob's factor in the auxiliary product state.
- auxLeft_normalized : self.auxLeft.IsNormalized
Alice's auxiliary factor is normalized.
- auxRight_normalized : self.auxRight.IsNormalized
Bob's auxiliary factor is normalized.
The auxiliary state is the product of its Alice and Bob factors.
The dilated bipartite state in the register order of the dilated measurements.
- dilatedState_density : self.dilatedState.density = naimarkProductExtensionDensity HA HB HauxA HauxB ψ self.auxState
The dilated state is
ψ ⊗ aux, with the four registers reassociated. - dilatedState_normalized : self.dilatedState.IsNormalized
The dilated state is normalized.
- left : IdxProjSubMeas QuestionA OutcomeA (HA.carrier × HauxA.carrier)
Alice's projective submeasurements on the enlarged Alice space.
- right : IdxProjSubMeas QuestionB OutcomeB (HB.carrier × HauxB.carrier)
Bob's projective submeasurements on the enlarged Bob space.
- correlation_preservation (x : QuestionA) (y : QuestionB) (a : OutcomeA) (b : OutcomeB) : ev ψ (opTensor ((A x).outcome a) ((B y).outcome b)) = ev self.dilatedState (opTensor ((self.left x).outcome a) ((self.right y).outcome b))
Preservation of the bipartite correlations for every question and outcome.
Instances For
Source-shaped statement of the full tensor-product Naimark theorem.
Paper origin: references/ldt-paper/orthonormalization.tex:36-80
(\label{thm:naimark}). The proof in the paper is the simultaneous
tensor-product assembly of the one-measurement helper, described at
references/ldt-paper/orthonormalization.tex:161-187.
The explicit normalization hypothesis records the paper convention that
\ket{\psi} is a state.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Orthonormalization statements #
Paper origin: references/ldt-paper/preliminaries.tex:348-376
(\label{def:approx_delta}) and references/ldt-paper/orthonormalization.tex
§4 prose around \label{lem:projective-non-measurement} (lines 414-538).
Conclusion of the intermediate almost-projective step: a measurement which is
ζ-strongly self-consistent and ζ-self-close in the state-dependent distance,
and whose effects satisfy Σₐ (Aₐ − Aₐ²) ≤ ζ.
- strongSelfConsistency : SSCRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) ζ
- selfDistance : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily A.toSubMeas) (2 * ζ)
Instances For
Paper origin: references/ldt-paper/orthonormalization.tex:414-538
(\label{lem:projective-non-measurement}); the truncation-function trunc_δ
itself is introduced inside the proof at lines 434-444, with the supporting
inequality \label{lem:trunc-inequality} at line 447.
Conclusion of the truncation-function step in the proof of rounding to projectors.
- roundedFamily : OpFamily Outcome ι
The operator family obtained by applying the truncation function to each effect.
- projective (a : Outcome) : Quantum.IsProj (self.roundedFamily.outcome a)
Each truncated effect is a projection.
- closeness : SDDOpRel ψ (uniformDistribution Unit) (fun (x : Unit) => A.toOpFamily) (fun (x : Unit) => self.roundedFamily) (2 * spectralTruncationError ζ)
The truncated family stays close to the input measurement in state-dependent operator distance, with the paper's
2√ζbound (references/ldt-paper/orthonormalization.tex:417). The stored total operator is the sum of the rounded family.
The total operator of the rounded family is almost bounded by
I.
Instances For
Paper origin: references/ldt-paper/orthonormalization.tex:414-538
(\label{lem:projective-non-measurement}).
Conclusion of the rounding-to-projective step: a genuine projective
sub-measurement P which is ζ-close to the input measurement A in the
state-dependent operator distance.
- closeness : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily P.toSubMeas) ζ
Instances For
Complete a submeasurement by adjoining the residual I - ∑ₐ Aₐ at the
fresh none outcome.
This is the completion used in the paper's proof of
thm:orthonormalization: the original outcomes are kept as some a, and the
missing mass is recorded separately at none.
Equations
- One or more equations did not get rendered due to their size.