Orthonormalization in a symmetric model of a finite pair, and membership #
Theorem G and Proposition H of reports/c6b-paper-proofs.md, §4 (Lemmas 14 and 15), stated for
any symmetric model whose bipartite reading is a finite pair, and specialized to the doubled model
Doubling.model hM hψ of Co/Doubling/Model.lean.
Theorem G (SymModel.orthonormalization_of_isFinitePair, in-core orthonormalization with the
vendored constant): in a symmetric model S whose bipartite reading S.toBipartite is a finite
pair whose first player's operators contain no nonzero abelian projection, a submeasurement X
of the local algebra whose bipartite strong self-consistency defect is at most ζ > 0 is within
orthonormalizationError ζ = 100 ζ^{1/4} of a projective submeasurement P of the same algebra:
∑_a ‖(L X_a − L P_a) Ψ‖² ≤ 100 ζ^{1/4}. SymModel.orthonormalization_of_isFinitePair_sddRel
states it in the vendored relations (BipartiteSSCRel to SDDRel at the one-point
distribution), the shape of the vendored MakingMeasurementsProjective.orthonormalization, which
milestone M8 ports. For the doubled model, Doubling.orthonormalization_model (both algebras of
M without abelian projections), Doubling.orthonormalization_model_sddRel and
Doubling.orthonormalization_of_isDyadicPair (a dyadic pair, whose algebras have no abelian
projection) specialize it. The proof (Lemma 14) completes X by the outcome none
(MakingMeasurementsProjective.optionCompletion), bounds the one-sided defect of the completion by
twice the bipartite defect of X (SymModel.one_sub_sum_norm_sq_completion_le), applies the
orthonormalization tier povm_orthogonalization_finitePair at ε = 3 min(ζ, 1), and drops the
outcome none (MakingMeasurementsProjective.restrictSomeProjSubMeas): 27 min(ζ, 1) ≤ 100 ζ^{1/4}. The hypothesis ζ > 0 is the strictness of the tier's hypothesis; the case ζ = 0
is not covered (report §4.7).
The completion and its restriction carry the names of their vendored counterparts and live in
the ports of those files, Co/MakingMeasurementsProjective/Statements.lean and
Co/MakingMeasurementsProjective/Orthonormalization/RestrictSome.lean, which this file imports.
Proposition H (membership): every continuous functional calculus of a local self-adjoint operator stays local.
- In a finite pair, the first player's operators are a commutant, closed under the functional
calculus (
Doubling.cfc_mem_opsA,Doubling.cfc_mem_opsB); - in a symmetric model with an injective placement, for instance the doubled model
(
Doubling.model_L_injective), the functional calculus of the local C⋆-algebra is the functional calculus of the operators:L (cfc f x) = cfc f (L x)(SymModel.L_cfc,SymModel.R_cfc), so thatcfc f (L x)is the placement of a local element (SymModel.cfc_L_mem_range) and, in the doubled model, order facts about it pull back alongDoubling.L_nonneg_iff(Theorem A.4).
The other two items of Proposition H are not statements here: ring operations stay in Loc M by
typing, and the orthonormalized measurement is supplied in Loc M by Theorem G; the semidefinite
witness Z is supplied by the summed form (planning/c6b-plan.md, M9).
The arithmetic of Theorem G #
27 min(ζ, 1) ≤ 100 ζ^{1/4} for ζ ≥ 0.
A unital ⋆-monomorphism of C⋆-algebras commutes with the real functional calculus of
self-adjoint elements, for every function (both sides vanish when the function is not continuous
on the spectrum, which the monomorphism preserves).
Theorem G and Proposition H in a symmetric model #
The second placement has the same state norms as the first: ‖R y Ψ‖ = ‖L y Ψ‖.
The bipartite self-overlap of a self-adjoint local element is at most its one-sided state
norm: ⟨Ψ, (y ⊗ y) Ψ⟩ ≤ ‖L y Ψ‖².
The one-sided defect of the completion is at most twice the bipartite defect
(Lemma 14, steps 1–3, of reports/c6b-paper-proofs.md, §4): for a submeasurement X,
1 − ∑_õ ‖L X̃_õ Ψ‖² ≤ 2 · qBipartiteSSCDefect X, where X̃ is the completion of X by none.
Orthonormalization in a symmetric model of a finite pair (Theorem G of
reports/c6b-paper-proofs.md, §4, Lemma 14): if the bipartite reading of S is a finite pair
whose first player's operators contain no nonzero abelian projection, a submeasurement X of the
local algebra with bipartite strong self-consistency defect at most ζ > 0 is within
orthonormalizationError ζ = 100 ζ^{1/4} of a projective submeasurement P of the local algebra:
∑_a ‖(L X_a − L P_a) Ψ‖² ≤ 100 ζ^{1/4}.
Orthonormalization in a symmetric model of a finite pair, in the vendored relations
(Theorem G, the shape of the vendored MakingMeasurementsProjective.orthonormalization): a
bipartite strong self-consistency relation at ζ > 0 for a constant family yields a projective
submeasurement whose left placement is within orthonormalizationError ζ in the state-dependent
distance.
The local functional calculus is the operator functional calculus (Proposition H of
reports/c6b-paper-proofs.md, §4): if the first placement is injective,
L (cfc f x) = cfc f (L x) for a self-adjoint local element x and every f : ℝ → ℝ.
The local functional calculus is the operator functional calculus for the second placement:
R (cfc f x) = cfc f (R x), if the first placement is injective.
The functional calculus of a placed local operator is placed (Proposition H): if the first placement is injective, it is the placement of the local functional calculus.
Proposition H in a finite pair #
The functional calculus stays in the first player's operators of a finite pair
(Proposition H of reports/c6b-paper-proofs.md, §4): they are the commutant of the second
player's (IsFinitePair.coe_centralizer_opsB), a closed ⋆-subalgebra.
The functional calculus stays in the second player's operators of a finite pair.
The functional calculus of the doubled local algebra is that of its C⋆-algebra structure; the
shortcut instances below make the real scalars, and so the real functional calculus, go through
CStarAlgebra (Loc M) rather than through the product (Prod.algebra), whose real algebra the
continuous functional calculus of a C⋆-algebra does not unify with.
The doubled local algebra is a real normed algebra, through its C⋆-algebra structure (shortcut).
The real algebra structure of the doubled local algebra, through its C⋆-algebra structure (shortcut).
The real continuous functional calculus of the doubled local algebra, that of a C⋆-algebra (shortcut).
The first placement of the doubled model is injective, so SymModel.L_cfc,
SymModel.R_cfc and SymModel.cfc_L_mem_range apply to it.
The second placement of the doubled model is injective.
Theorem G in the doubled model #
Orthonormalization in the doubled model (Theorem G of reports/c6b-paper-proofs.md, §4,
Lemma 14): if neither algebra of the finite pair M has a nonzero abelian projection, a
submeasurement X of the doubled local algebra with bipartite strong self-consistency defect at
most ζ > 0 is within orthonormalizationError ζ = 100 ζ^{1/4} of a projective submeasurement P
of the doubled local algebra: ∑_a ‖(L X_a − L P_a) Ψ‖² ≤ 100 ζ^{1/4}.
Orthonormalization in the doubled model of a dyadic pair (Theorem G): the algebras of a
dyadic pair have no abelian projection (IsDyadicPair.noAbelianProj_opsA).
Orthonormalization in the doubled model, in the vendored relations (Theorem G, the model
form of the vendored MakingMeasurementsProjective.orthonormalization): a bipartite strong
self-consistency relation at ζ > 0 for a constant family yields a projective submeasurement
whose left placement is within orthonormalizationError ζ in the state-dependent distance.