The doubled model of a finite pair #
The vendored low-individual-degree core assumes a state fixed by the swap of two identical tensor
factors. The port supplies that symmetry for any finite pair M by doubling it
(reports/c6b-paper-proofs.md, §4; planning/c6b-plan.md, M2): the doubled model D(M) acts on
H ⊕ H, its first player by u ⊕ v and its second by v ⊕ u, its state is (ψ, ψ)/√2, and the
flip (ξ, η) ↦ (η, ξ) fixes the state and exchanges the players. This file builds it as a
symmetric model of the port (SymModel, Co/Basic/QuantumState.lean) and proves the formulas
that later stages read through it; Co/Doubling/FinitePair.lean shows that it is again a finite
pair, and Co/Doubling/Halving.lean relates its quantities to those of M.
The local algebra. The report states D(M) over the abstract product 𝒜 × ℬ; a symmetric model
needs a C⋆-algebra. So the local algebra is Loc M = LocA M × LocB M, where LocA M is the
commutant of the second player's operators of M and LocB M the commutant of the first player's:
closed ⋆-subalgebras of B(H), so C⋆-algebras, star-ordered with the operator order
(MIPRE/Foundations/FinitePairOrder.lean). In a finite pair they are the players' operators, and
𝒜 ≃⋆ₐ LocA M, ℬ ≃⋆ₐ LocB M preserve and reflect the order (IsFinitePair.equivA,
IsFinitePair.equivB); Co/Doubling/FinitePair.lean assembles them into 𝒜 × ℬ ≃⋆ₐ Loc M.
The model (Doubling.model M hM hψ): K = Ampl (Fin 2) M.H = H ⊕ H, Ψ = halfVec ψ,
L (a, b) = a ⊕ b (model_L), J = flip2, so that R (a, b) = b ⊕ a (model_R). The two
placements commute because in a finite pair LocA M and LocB M are the two players' operators,
which commute (commute_locA_locB); this is the only place the finite-pair hypothesis enters the
definition.
Formulas (Lemmas 2 and 5 of the report, Theorem C):
ev_diag2: the expectation of a block-diagonal operator is the average of its blocks' expectations atψ; soev (L x) = ½ (⟨x₁⟩ + ⟨x₂⟩)(ev_L) and the same forR(ev_R);inner_L_mul_R,ev_L_mul_R(the role average):⟪Ψ, L x R y Ψ⟫ = ½ (⟪ψ, x₁ y₂ ψ⟫ + ⟪ψ, y₁ x₂ ψ⟫);bornProb_model: the Born probability of the doubled model is the average of the two operator Born probabilities.
The local algebra and the placement #
The first player's block of the doubled local algebra: the commutant of the second player's
operators of M (in a finite pair, the first player's operators).
Equations
Instances For
The second player's block of the doubled local algebra: the commutant of the first player's
operators of M (in a finite pair, the second player's operators).
Equations
Instances For
The local algebra of the doubled model, LocA M × LocB M: a C⋆-algebra, star-ordered
componentwise with the operator order.
Equations
Instances For
The structure of Loc M is that of a C⋆-algebra; the shortcut instances below make every
synthesis of its ring, star and algebra structure go through CStarAlgebra (Loc M), the path the
symmetric model SymModel (Loc M) _ and its bipartite model are stated with, rather than through
the product, so that the two need no unfolding to be compared.
The doubled local algebra is a C⋆-algebra (shortcut).
The ring structure of the doubled local algebra, through its C⋆-algebra structure (shortcut).
The star structure of the doubled local algebra, through its C⋆-algebra structure (shortcut).
The complex algebra structure of the doubled local algebra, through its C⋆-algebra structure (shortcut).
The order of the doubled local algebra: componentwise (shortcut).
The doubled local algebra is star-ordered (shortcut).
The first block of an element of the doubled local algebra, as an operator.
Equations
Instances For
The second block of an element of the doubled local algebra, as an operator.
Equations
Instances For
The first placement of the doubled model, (a, b) ↦ a ⊕ b, a unital ⋆-homomorphism.
Equations
Instances For
In a finite pair the two blocks commute: LocA M is the first player's operators, and
LocB M commutes with them.
The doubled model D(M) of a finite pair with a unit state (reports/c6b-paper-proofs.md,
§4.1): on H ⊕ H, with the state (ψ, ψ)/√2, the first placement (a, b) ↦ a ⊕ b of
Loc M = LocA M × LocB M, and the flip of the two copies.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The state of the doubled model is the half vector (ψ, ψ)/√2.
The first placement of the doubled model: L (a, b) = a ⊕ b.
The second placement of the doubled model: R (a, b) = b ⊕ a.
Expectations #
The state formula (Lemma 2 of reports/c6b-paper-proofs.md, §4.3): the expectation of a
block-diagonal operator is the average of its blocks' expectations at ψ.
The expectation of the first placement is the average of the blocks' expectations.
The expectation of the second placement is the average of the blocks' expectations.
The product of the two placements is block diagonal:
L x R y = (x₁ y₂) ⊕ (y₁ x₂).
The role average (Theorem C, Lemma 5 of reports/c6b-paper-proofs.md, §4):
⟪Ψ, L x R y Ψ⟫ = ½ (⟪ψ, x₁ y₂ ψ⟫ + ⟪ψ, y₁ x₂ ψ⟫).
The role average, for the expectation: ev (L x R y) = ½ (⟨x₁ y₂⟩ + ⟨y₁ x₂⟩).
The Born probability of the doubled model is the average of the operator Born probabilities of the two role assignments.