Readings of an extended model along a regrouping of its registers #
An extension M.expand e of a bipartite model by a register α for the first player and a
register β for the second (MIPRE/Foundations/AncillaModel.lean) fixes which registers each
player holds. The soundness analysis of the Pauli basis test reads one state along several such
assignments, its cuts: a register handed across the cut is read by the other player, and nothing
happens to the state. New in Phase 5 of planning/mipco-track.md, where the analysis is stated in
a bipartite model; this file is the model form of the matrix regroupings of the registers
(Matrix.reindex along Equiv.prodAssoc and its relatives) of that analysis.
- A reading (
BipartiteModel.recut): along a bijectionσ : α × β ≃ α' × β', the state model ofM.expand e, its space, state and representation unchanged, with the first player'sα' × α'matrices and the second'sβ' × β'matrices acting throughσ. What is computed in the state model (state norms, quadratic forms) is shared by all the readings of one extension. The entries of a reading are those of the extension read throughσ(recut_πA_apply,recut_πB_apply; for the extension itselfexpand_πA_apply,expand_πB_apply,expand_πA_mul_πB_apply). - Handing the first player's outer register to the second player (
moveEquiv): the operators of that reading are operators of the extension (recut_move_πA,recut_move_πB), so an operator of one cut that is a product on the moved register is a product of the two players' operators of the other. WithsmulKron_eq_diagonal_mulandcompHom_smulKron_one, these two lemmas are every change of cut the analysis makes. - A reading is isomorphic to the extension along the regrouped registers
(
BipartiteModel.recutIso, from the local isometryBipartiteModel.recutIsom): the reindexing of theℓ²sum, the players' algebras unchanged. - The two-sided compression (
BipartiteModel.bornProb_expand_basisVec): on the extension at a product basis vector (basisVec), a Born probability is the Born probability of the two reference entries.
Reindexing square matrices over a ⋆-algebra #
Matrix.reindex over a ⋆-algebra, as a unital ⋆-algebra homomorphism: the homomorphism
underlying submatrixStarAlgEquiv σ.symm (MIPRE/Foundations/ModelIso.lean), as πA and πB
of a model are unital.
Equations
- MIPRE.reindexStarAlgHomR σ = { toAlgHom := ↑(Matrix.reindexAlgEquiv ℂ R σ), map_star' := ⋯ }
Instances For
Register operators as block matrices #
X ⊗ P is (X ⊗ 1)(1 ⊗ P): the element on the diagonal, times the register operator.
A register operator of the outer register, tensored with an element and a register operator of
the inner one, is one register operator of the pair of registers (Matrix.comp).
A register operator of the outer register is a register operator of the pair, acting as the identity on the inner register.
Moving a register across the cut, and product basis vectors #
The regrouping of registers handing the first player's outer register γ to the second
player: ((c, a), b) ↦ (a, (c, b)).
Equations
Instances For
The basis vector |a₀⟩ ⊗ |b₀⟩ of a pair of registers.
Instances For
Exchanging the two registers exchanges the two reference points.
A product basis vector is a unit vector.
Readings of an extension #
The reading of an extension along a regrouping of its registers: the state model of
M.expand e (its space, state and representation), with the first player's α' × α' matrices and
the second player's β' × β' matrices acting through the bijection σ : α × β ≃ α' × β'. Two
readings of one extension differ only in their players' representations.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Every reading of an extension has the extension's state model.
The first player's operators of a reading, entry by entry.
The second player's operators of a reading, entry by entry.
The first player's operators of an extension, entry by entry.
The second player's operators of an extension, entry by entry.
A product of the two players' operators of an extension, entry by entry.
Moving the first player's outer register to the second player #
Reading lemma for the first player: once the first player's outer register γ is handed
to the second player, an operator X of the first player's remaining register α₀ is the
extension's operator 1_γ ⊗ X.
Reading lemma for the second player: once the first player's outer register γ is handed
to the second player, an operator of the second player that is a product Q ⊗ Y of a register
operator Q of γ and an operator Y of the second player's own registers is the product of the
extension's first-player operator Q ⊗ 1 and second-player operator Y.
A reading is isomorphic to the extension along the regrouped registers #
The Hilbert space of a reading is the ℓ² sum (as for the extension, BipartiteModel.ampl).
Instances For
The change of cut as a local isometry: the extension along the regrouped registers onto
the reading of the original extension, by the reindexing of the ℓ² sum, the players' algebras
unchanged.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The change of cut carries the state to the state.
A reading of an extension is isomorphic to the extension along the regrouped registers:
the reindexing of the ℓ² sum, with the players' algebras unchanged (recutIsom).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The two-sided compression at a product basis vector #
The two-sided compression: on the extension at a product basis vector |a₀⟩ ⊗ |b₀⟩, a
Born probability is the Born probability of the two reference entries.
The value of a strategy of an extension at a product basis vector is the value of the families of its reference entries.
On an extension at a product basis vector, two families with the same reference entries have the same inconsistency: a Born probability sees only the reference entries.