Documentation

MIPRE.Background.LIDT.MIPStarRE.LDT.Test.StrategyBiProj.DirectSum

Two-Space Projective Strategies: Direct-Sum State Blocks #

This module contains the role-register direct-sum carriers and block-state construction used to symmetrize a heterogeneous projective strategy.

Direct-sum role-register helpers #

source
@[reducible, inline]
abbrev MIPStarRE.LDT.ProjStrat.LocalCarrierSum (ιA : Type u_1) (ιB : Type u_2) :
Type (max u_1 u_2)

Direct-sum carrier for the future heterogeneous role symmetrization.

For a two-space strategy with Alice carrier ιA and Bob carrier ιB, the later symmetrized local space will use this tagged direct sum so that Alice's operators occupy the Sum.inl block and Bob's operators occupy the Sum.inr block.

Equations
Instances For
    source
    @[reducible, inline]
    abbrev MIPStarRE.LDT.ProjStrat.RoleRegisterLocal (ιA : Type u_1) (ιB : Type u_2) :
    Type (max u_2 u_1)

    Local carrier planned for the heterogeneous symmetrization bridge: a role bit and a direct-sum carrier. This is the direct-sum analogue of the current same-space target Role × ι in StrategyRole.lean.

    Equations
    Instances For
      source
      def MIPStarRE.LDT.ProjStrat.roleRegisterPairLocalEquiv (ιA : Type u_1) (ιB : Type u_2) :
      (Role × Role) × LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB ≃ RoleRegisterLocal ιA ιB × RoleRegisterLocal ιA ιB

      Reassociate role bits and direct-sum carriers.

      This is the public heterogeneous analogue of the same-space role-register reassociation used internally by StrategyRole.lean. It prepares the target shape for reindexing block states on (Role × (ιA ⊕ ιB)) × (Role × (ιA ⊕ ιB)).

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Direct-sum block states for heterogeneous role symmetrization #

        source
        noncomputable def MIPStarRE.LDT.ProjStrat.localPairABBlock {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) :
        Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)

        Embed an operator on Alice's and Bob's original tensor product into the (Sum.inl _) × (Sum.inr _) block of the direct-sum tensor product.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          noncomputable def MIPStarRE.LDT.ProjStrat.localPairBABlock {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιB × ιA)) :
          Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)

          Embed an operator on Bob's and Alice's original tensor product into the (Sum.inr _) × (Sum.inl _) block of the direct-sum tensor product.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairABBlock_AB_AB {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) (i i' : ιA) (j j' : ιB) :
            localPairABBlock X (Sum.inl i, Sum.inr j) (Sum.inl i', Sum.inr j') = X (i, j) (i', j')
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairBABlock_BA_BA {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιB × ιA)) (i i' : ιB) (j j' : ιA) :
            localPairBABlock X (Sum.inr i, Sum.inl j) (Sum.inr i', Sum.inl j') = X (i, j) (i', j')
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairABBlock_conjTranspose {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) :
            Matrix.conjTranspose (localPairABBlock X) = localPairABBlock (Matrix.conjTranspose X)
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairBABlock_conjTranspose {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιB × ιA)) :
            Matrix.conjTranspose (localPairBABlock X) = localPairBABlock (Matrix.conjTranspose X)
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairABBlock_mul {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X Y : Quantum.Op (ιA × ιB)) :
            localPairABBlock X * localPairABBlock Y = localPairABBlock (X * Y)
            source
            @[simp]
            theorem MIPStarRE.LDT.ProjStrat.localPairBABlock_mul {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X Y : Quantum.Op (ιB × ιA)) :
            localPairBABlock X * localPairBABlock Y = localPairBABlock (X * Y)
            source
            theorem MIPStarRE.LDT.ProjStrat.localPairABBlock_nonneg {ιA : Type u_1} {ιB : Type u_2} [Finite ιA] [Finite ιB] {X : Quantum.Op (ιA × ιB)} (hX : 0 ≤ X) :
            0 ≤ localPairABBlock X
            source
            theorem MIPStarRE.LDT.ProjStrat.localPairBABlock_nonneg {ιA : Type u_1} {ιB : Type u_2} [Finite ιA] [Finite ιB] {X : Quantum.Op (ιB × ιA)} (hX : 0 ≤ X) :
            0 ≤ localPairBABlock X
            source
            noncomputable def MIPStarRE.LDT.ProjStrat.heterogeneousSwapDensity {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) :
            Quantum.Op (ιB × ιA)

            Swap an operator on ιA × ιB to one on ιB × ιA.

            Equations
            Instances For
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.heterogeneousSwapDensity_opTensor {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : Quantum.Op ιA) (B : Quantum.Op ιB) :
              heterogeneousSwapDensity (opTensor A B) = opTensor B A

              Lean-only: Tensor products commute with the heterogeneous swap map.

              Paper origin: references/ldt-paper/inductive_step.tex:40-66; this is the matrix-index identity used to identify the two role-register sectors in the heterogeneous symmetrization.

              source
              theorem MIPStarRE.LDT.ProjStrat.heterogeneousSwapDensity_nonneg {ιA : Type u_1} {ιB : Type u_2} [Finite ιA] [Finite ιB] {X : Quantum.Op (ιA × ιB)} (hX : 0 ≤ X) :
              0 ≤ heterogeneousSwapDensity X
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.heterogeneousSwapDensity_mul {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X Y : Quantum.Op (ιA × ιB)) :
              heterogeneousSwapDensity (X * Y) = heterogeneousSwapDensity X * heterogeneousSwapDensity Y
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.swapDensity_localPairABBlock {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) :
              swapDensity (localPairABBlock X) = localPairBABlock (heterogeneousSwapDensity X)
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.swapDensity_localPairBABlock_heterogeneousSwapDensity {ιA : Type u_1} {ιB : Type u_2} (X : Quantum.Op (ιA × ιB)) :
              swapDensity (localPairBABlock (heterogeneousSwapDensity X)) = localPairABBlock X
              source
              theorem MIPStarRE.LDT.ProjStrat.trace_localPairABBlock {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X : Quantum.Op (ιA × ιB)) :
              Matrix.trace (localPairABBlock X) = Matrix.trace X
              source
              theorem MIPStarRE.LDT.ProjStrat.trace_localPairBABlock {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X : Quantum.Op (ιB × ιA)) :
              Matrix.trace (localPairBABlock X) = Matrix.trace X
              source
              theorem MIPStarRE.LDT.ProjStrat.normalizedTrace_localPairABBlock {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Nonempty ιA] [Fintype ιB] [Nonempty ιB] (X : Quantum.Op (ιA × ιB)) :
              Quantum.normalizedTrace (localPairABBlock X) = ↑(Fintype.card ιA) * ↑(Fintype.card ιB) / ↑(Fintype.card (LocalCarrierSum ιA ιB)) ^ 2 * Quantum.normalizedTrace X
              source
              theorem MIPStarRE.LDT.ProjStrat.normalizedTrace_localPairBABlock {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Nonempty ιA] [Fintype ιB] [Nonempty ιB] (X : Quantum.Op (ιB × ιA)) :
              Quantum.normalizedTrace (localPairBABlock X) = ↑(Fintype.card ιA) * ↑(Fintype.card ιB) / ↑(Fintype.card (LocalCarrierSum ιA ιB)) ^ 2 * Quantum.normalizedTrace X
              source
              theorem MIPStarRE.LDT.ProjStrat.normalizedTrace_heterogeneousSwapDensity {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (X : Quantum.Op (ιA × ιB)) :
              Quantum.normalizedTrace (heterogeneousSwapDensity X) = Quantum.normalizedTrace X
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.rolePairProj_AB_mul_BA :
              rolePairProj Role.A Role.B * rolePairProj Role.B Role.A = 0
              source
              @[simp]
              theorem MIPStarRE.LDT.ProjStrat.rolePairProj_BA_mul_AB :
              rolePairProj Role.B Role.A * rolePairProj Role.A Role.B = 0
              source
              noncomputable def MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (rL rR : Role) (X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
              Quantum.Op (RoleRegisterLocal ιA ιB × RoleRegisterLocal ιA ιB)

              Place a direct-sum bipartite operator in a chosen pair of role sectors.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond_nonneg {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (rL rR : Role) {X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)} (hX : 0 ≤ X) :
                0 ≤ rolePairDirectSumCond rL rR X
                source
                theorem MIPStarRE.LDT.ProjStrat.normalizedTrace_rolePairDirectSumCond {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] (rL rR : Role) (X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
                Quantum.normalizedTrace (rolePairDirectSumCond rL rR X) = 1 / 4 * Quantum.normalizedTrace X
                source
                @[simp]
                theorem MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond_mul_same {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (rL rR : Role) (X Y : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
                rolePairDirectSumCond rL rR X * rolePairDirectSumCond rL rR Y = rolePairDirectSumCond rL rR (X * Y)
                source
                theorem MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond_mul_eq_zero_of_ne {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (rL rR sL sR : Role) (X Y : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) (h : (rL, rR) ≠ (sL, sR)) :
                rolePairDirectSumCond rL rR X * rolePairDirectSumCond sL sR Y = 0

                Distinct role-pair sectors of the direct-sum role register are orthogonal.

                source
                @[simp]
                theorem MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond_AB_mul_BA {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (X Y : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
                rolePairDirectSumCond Role.A Role.B X * rolePairDirectSumCond Role.B Role.A Y = 0
                source
                @[simp]
                theorem MIPStarRE.LDT.ProjStrat.rolePairDirectSumCond_BA_mul_AB {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (X Y : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
                rolePairDirectSumCond Role.B Role.A X * rolePairDirectSumCond Role.A Role.B Y = 0
                source
                @[simp]
                theorem MIPStarRE.LDT.ProjStrat.swapDensity_rolePairDirectSumCond {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (rL rR : Role) (X : Quantum.Op (LocalCarrierSum ιA ιB × LocalCarrierSum ιA ιB)) :
                swapDensity (rolePairDirectSumCond rL rR X) = rolePairDirectSumCond rR rL (swapDensity X)
                source
                noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterDensityScale (ιA : Type u_1) (ιB : Type u_2) [Fintype ιA] [Fintype ιB] :
                Error

                Normalizing scalar for the direct-sum heterogeneous role-register state.

                Equations
                Instances For
                  source
                  theorem MIPStarRE.LDT.ProjStrat.roleRegisterDensityScale_nonneg (ιA : Type u_1) (ιB : Type u_2) [Fintype ιA] [Fintype ιB] :
                  0 ≤ roleRegisterDensityScale ιA ιB
                  source
                  noncomputable def MIPStarRE.LDT.ProjStrat.roleRegisterSymmState {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) :
                  QuantumState (RoleRegisterLocal ιA ιB × RoleRegisterLocal ιA ιB)

                  Heterogeneous role-register symmetrization of a two-space bipartite state.

                  The state lives on Role × (ιA ⊕ ιB) on each side. Its occupied sectors are A/B, carrying the original density in the Sum.inl × Sum.inr direct-sum block, and B/A, carrying the swapped density in the Sum.inr × Sum.inl block. The scalar compensates for normalized trace on the enlarged direct-sum carrier. Normalization and the LDT goodness comparison are separate lemmas.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[simp]
                    theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmState_density_fixed {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) :
                    swapDensity (roleRegisterSymmState ψ).density = (roleRegisterSymmState ψ).density
                    source
                    theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmState_permInvState {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) :
                    PermInvState (roleRegisterSymmState ψ)
                    source
                    theorem MIPStarRE.LDT.ProjStrat.roleRegisterSymmState_isNormalized {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Nonempty ιA] [Fintype ιB] [DecidableEq ιB] [Nonempty ιB] (ψ : QuantumState (ιA × ιB)) (hψ : ψ.IsNormalized) :
                    (roleRegisterSymmState ψ).IsNormalized
                    source
                    noncomputable def MIPStarRE.LDT.ProjStrat.localDirectSumBlock {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) :
                    Quantum.Op (LocalCarrierSum ιA ιB)

                    Block-diagonal operator on ιA ⊕ ιB, with Alice's block in the Sum.inl sector and Bob's block in the Sum.inr sector.

                    This is the matrix-level direct sum that will underlie symmetrized measurements such as |0⟩⟨0| ⊗ A^A + |1⟩⟨1| ⊗ A^B from references/ldt-paper/inductive_step.tex:55-59.

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_inl_inl {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) (i j : ιA) :
                      localDirectSumBlock A B (Sum.inl i) (Sum.inl j) = A i j
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_inl_inr {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) (i : ιA) (j : ιB) :
                      localDirectSumBlock A B (Sum.inl i) (Sum.inr j) = 0
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_inr_inl {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) (i : ιB) (j : ιA) :
                      localDirectSumBlock A B (Sum.inr i) (Sum.inl j) = 0
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_inr_inr {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) (i j : ιB) :
                      localDirectSumBlock A B (Sum.inr i) (Sum.inr j) = B i j
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_one {ιA : Type u_1} {ιB : Type u_2} [DecidableEq ιA] [DecidableEq ιB] :
                      localDirectSumBlock 1 1 = 1
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_zero {ιA : Type u_1} {ιB : Type u_2} :
                      localDirectSumBlock 0 0 = 0
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_add {ιA : Type u_1} {ιB : Type u_2} (A₁ A₂ : Quantum.Op ιA) (B₁ B₂ : Quantum.Op ιB) :
                      localDirectSumBlock A₁ B₁ + localDirectSumBlock A₂ B₂ = localDirectSumBlock (A₁ + A₂) (B₁ + B₂)

                      Direct-sum blocks are additive in the two diagonal blocks.

                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_conjTranspose {ιA : Type u_1} {ιB : Type u_2} (A : Quantum.Op ιA) (B : Quantum.Op ιB) :
                      Matrix.conjTranspose (localDirectSumBlock A B) = localDirectSumBlock (Matrix.conjTranspose A) (Matrix.conjTranspose B)
                      source
                      @[simp]
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_mul {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (A₁ A₂ : Quantum.Op ιA) (B₁ B₂ : Quantum.Op ιB) :
                      localDirectSumBlock A₁ B₁ * localDirectSumBlock A₂ B₂ = localDirectSumBlock (A₁ * A₂) (B₁ * B₂)
                      source
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_nonneg {ιA : Type u_1} {ιB : Type u_2} [Finite ιA] [Finite ιB] {A : Quantum.Op ιA} {B : Quantum.Op ιB} (hA : 0 ≤ A) (hB : 0 ≤ B) :
                      0 ≤ localDirectSumBlock A B

                      A direct sum of positive semidefinite operators is positive semidefinite.

                      source
                      theorem MIPStarRE.LDT.ProjStrat.localDirectSumBlock_finset_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} (s : Finset α) (A : α → Quantum.Op ιA) (B : α → Quantum.Op ιB) :
                      ∑ a ∈ s, localDirectSumBlock (A a) (B a) = localDirectSumBlock (∑ a ∈ s, A a) (∑ a ∈ s, B a)

                      Finite sums commute through direct-sum blocks.

                      This is the completeness calculation for block-diagonal measurements: if Alice's and Bob's effects each sum to their local totals, then the direct-sum effects sum to the direct sum of those totals.

                      source
                      noncomputable def MIPStarRE.LDT.ProjStrat.roleBlock {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) :
                      Quantum.Op (RoleRegisterLocal ιA ιB)

                      Role-blocked operator on Role × (ιA ⊕ ιB).

                      The first block is used when the role register is Role.A; the second block is used when the role register is Role.B. This is the direct-sum scaffold for the paper's symmetrized measurements in inductive_step.tex:55-59.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_A {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) (i j : LocalCarrierSum ιA ιB) :
                        roleBlock A B (Role.A, i) (Role.A, j) = A i j
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_B {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) (i j : LocalCarrierSum ιA ιB) :
                        roleBlock A B (Role.B, i) (Role.B, j) = B i j
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_AB {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) (i j : LocalCarrierSum ιA ιB) :
                        roleBlock A B (Role.A, i) (Role.B, j) = 0
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_BA {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) (i j : LocalCarrierSum ιA ιB) :
                        roleBlock A B (Role.B, i) (Role.A, j) = 0
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_one {ιA : Type u_1} {ιB : Type u_2} [DecidableEq ιA] [DecidableEq ιB] :
                        roleBlock 1 1 = 1
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_zero {ιA : Type u_1} {ιB : Type u_2} :
                        roleBlock 0 0 = 0
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_add {ιA : Type u_1} {ιB : Type u_2} (A₁ A₂ B₁ B₂ : Quantum.Op (LocalCarrierSum ιA ιB)) :
                        roleBlock A₁ B₁ + roleBlock A₂ B₂ = roleBlock (A₁ + A₂) (B₁ + B₂)

                        Role-register blocks are additive in their two role sectors.

                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_conjTranspose {ιA : Type u_1} {ιB : Type u_2} (A B : Quantum.Op (LocalCarrierSum ιA ιB)) :
                        Matrix.conjTranspose (roleBlock A B) = roleBlock (Matrix.conjTranspose A) (Matrix.conjTranspose B)
                        source
                        @[simp]
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_mul {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [Fintype ιB] (A₁ A₂ B₁ B₂ : Quantum.Op (LocalCarrierSum ιA ιB)) :
                        roleBlock A₁ B₁ * roleBlock A₂ B₂ = roleBlock (A₁ * A₂) (B₁ * B₂)
                        source
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_nonneg {ιA : Type u_1} {ιB : Type u_2} [Finite ιA] [Finite ιB] {A B : Quantum.Op (LocalCarrierSum ιA ιB)} (hA : 0 ≤ A) (hB : 0 ≤ B) :
                        0 ≤ roleBlock A B

                        A role block of positive semidefinite operators is positive semidefinite.

                        source
                        theorem MIPStarRE.LDT.ProjStrat.roleBlock_finset_sum {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} (s : Finset α) (A B : α → Quantum.Op (LocalCarrierSum ιA ιB)) :
                        ∑ a ∈ s, roleBlock (A a) (B a) = roleBlock (∑ a ∈ s, A a) (∑ a ∈ s, B a)

                        Finite sums commute through role-register blocks.

                        This is the role-sector analogue of localDirectSumBlock_finset_sum and is the main completeness calculation for role-blocked measurements.