Unital dyadic matrix units

The orthonormalization step of the C6b port (planning/c6b-plan.md, §1, item 2) applies only in algebras without nonzero abelian projections, and the class of models it is run in is cut out by a purely algebraic condition that excludes them: unital 2ⁿ × 2ⁿ matrix units for every n (reports/c6b-paper-proofs.md, §3). This file is that condition and its algebra; the trace estimate that turns it into the absence of abelian projections is MIPRE/Foundations/DyadicPair.lean.

• IsMatUnits e: a family e : ι → ι → A of a ⋆-ring is a system of unital matrix units, eᵢⱼ eₗₘ = [j = l] eᵢₘ, eᵢⱼ⋆ = eⱼᵢ, ∑ᵢ eᵢᵢ = 1.
• HasDyadicUnits A: A has unital matrix units indexed by Fin n → Fin 2, for every n. Indexing by bit strings, rather than by Fin (2 ^ n), is what makes the tensor-product construction below a plain recursion.
• Transports. The condition passes along unital ⋆-homomorphisms (HasDyadicUnits.map), to the opposite ring (.op, transposing), to square matrices over the ring (.matrix, as scalar diagonals: the first player's algebra of an ancilla extension M.expand e) and to products (.prod).
• Pauli sites. A ⋆-algebra with a self-adjoint anticommuting pair of symmetries (xₖ, zₖ) at each site k : ℕ, pairs at distinct sites commuting (PauliSites), has dyadic units (PauliSites.hasDyadicUnits): the single-site units are xᵃ p xᵇ with p = (1 + z)/2, and the 2ⁿ × 2ⁿ units are their products over the sites 0, …, n - 1. This is how the twisted Pauli algebra of the value lemma's amplification gets its units.

Unital matrix units

structure MIPRE.IsMatUnits {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (e : ι → ι → A) : Prop

Unital matrix units (def:dyadic-units) in a ⋆-ring, indexed by a finite type ι: eᵢⱼ eₗₘ = [j = l] eᵢₘ, eᵢⱼ⋆ = eⱼᵢ and ∑ᵢ eᵢᵢ = 1.

• mul (i j l m : ι) : e i j * e l m = if j = l then e i m else 0

  The multiplication rule eᵢⱼ eₗₘ = [j = l] eᵢₘ.

• star_eq (i j : ι) : star (e i j) = e j i

  The adjoint rule eᵢⱼ⋆ = eⱼᵢ.

• sum_diag : ∑ i : ι, e i i = 1

  The units are unital: ∑ᵢ eᵢᵢ = 1.

theorem MIPRE.IsMatUnits.mul_cancel {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → ι → A} (he : IsMatUnits e) (i j m : ι) : e i j * e j m = e i m

eᵢⱼ eⱼₘ = eᵢₘ.

theorem MIPRE.IsMatUnits.map {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → ι → A} (he : IsMatUnits e) {B : Type u_3} {F : Type u_4} [Ring B] [StarRing B] [FunLike F A B] [RingHomClass F A B] [StarHomClass F A B] (φ : F) : IsMatUnits fun (i j : ι) => φ (e i j)

Matrix units pass along a unital ⋆-homomorphism (lem:dyadic-units-closure).

theorem MIPRE.IsMatUnits.op {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → ι → A} (he : IsMatUnits e) : IsMatUnits fun (i j : ι) => MulOpposite.op (e j i)

Transposed matrix units in the opposite ring (lem:dyadic-units-closure): eᵢⱼ ↦ op eⱼᵢ.

theorem MIPRE.IsMatUnits.diagonal {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → ι → A} (he : IsMatUnits e) (α : Type u_3) [Fintype α] [DecidableEq α] : IsMatUnits fun (i j : ι) => Matrix.diagonal fun (x : α) => e i j

Scalar-diagonal amplification (lem:dyadic-units-closure): eᵢⱼ ↦ diag(eᵢⱼ, …, eᵢⱼ) in the α × α matrices.

theorem MIPRE.IsMatUnits.prod {A : Type u_1} [Ring A] [StarRing A] {ι : Type u_2} [Fintype ι] [DecidableEq ι] {e : ι → ι → A} (he : IsMatUnits e) {B : Type u_3} [Ring B] [StarRing B] {f : ι → ι → B} (hf : IsMatUnits f) : IsMatUnits fun (i j : ι) => (e i j, f i j)

Componentwise matrix units in a product (lem:dyadic-units-closure): eᵢⱼ ↦ (eᵢⱼ, fᵢⱼ).

Dyadic matrix units

def MIPRE.HasDyadicUnits (A : Type u_1) [Ring A] [StarRing A] : Prop

Unital dyadic matrix units (def:dyadic-units): a ⋆-ring has unital matrix units of size 2ⁿ for every n, indexed by the bit strings Fin n → Fin 2.

Equations

• MIPRE.HasDyadicUnits A = ∀ (n : ℕ), ∃ (e : (Fin n → Fin 2) → (Fin n → Fin 2) → A), MIPRE.IsMatUnits e

theorem MIPRE.HasDyadicUnits.map {A : Type u_1} [Ring A] [StarRing A] (h : HasDyadicUnits A) {B : Type u_2} {F : Type u_3} [Ring B] [StarRing B] [FunLike F A B] [RingHomClass F A B] [StarHomClass F A B] (φ : F) : HasDyadicUnits B

Dyadic units pass along a unital ⋆-homomorphism (lem:dyadic-units-closure).

theorem MIPRE.HasDyadicUnits.op {A : Type u_1} [Ring A] [StarRing A] (h : HasDyadicUnits A) : HasDyadicUnits Aᵐᵒᵖ

Dyadic units pass to the opposite ring (lem:dyadic-units-closure).

theorem MIPRE.HasDyadicUnits.matrix {A : Type u_1} [Ring A] [StarRing A] (h : HasDyadicUnits A) (α : Type u_2) [Fintype α] [DecidableEq α] : HasDyadicUnits (Matrix α α A)

Dyadic units pass to square matrices over the ring (lem:dyadic-units-closure), as scalar diagonals.

theorem MIPRE.HasDyadicUnits.prod {A : Type u_1} [Ring A] [StarRing A] (h : HasDyadicUnits A) {B : Type u_2} [Ring B] [StarRing B] (hB : HasDyadicUnits B) : HasDyadicUnits (A × B)

Dyadic units pass to products (lem:dyadic-units-closure), componentwise.

Dyadic units from Pauli sites

structure MIPRE.PauliSites (R : Type u_1) [Ring R] [StarRing R] : Type u_1

Pauli sites (lem:pauli-sites-units) in a ⋆-ring: at each site k : ℕ a self-adjoint anticommuting pair of symmetries (x k, z k), the pairs at distinct sites commuting.

• x : ℕ → R

  The X symmetry at each site.

• z : ℕ → R

  The Z symmetry at each site.

• x_mul_self (k : ℕ) : self.x k * self.x k = 1

  xₖ² = 1.

• z_mul_self (k : ℕ) : self.z k * self.z k = 1

  zₖ² = 1.

• z_mul_x (k : ℕ) : self.z k * self.x k = -(self.x k * self.z k)

  xₖ and zₖ anticommute.

• star_x (k : ℕ) : star (self.x k) = self.x k

  xₖ is self-adjoint.

• star_z (k : ℕ) : star (self.z k) = self.z k

  zₖ is self-adjoint.

• commute_x_x (k l : ℕ) : k ≠ l → Commute (self.x k) (self.x l)

  The X symmetries at distinct sites commute.

• commute_x_z (k l : ℕ) : k ≠ l → Commute (self.x k) (self.z l)

  The X and Z symmetries at distinct sites commute.

• commute_z_z (k l : ℕ) : k ≠ l → Commute (self.z k) (self.z l)

  The Z symmetries at distinct sites commute.

noncomputable def MIPRE.PauliSites.proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) : R

The projection pₖ = (1 + zₖ)/2.

Equations

• S.proj k = 2⁻¹ • (1 + S.z k)

def MIPRE.PauliSites.xpow {R : Type u_1} [Ring R] [StarRing R] (S : PauliSites R) (k : ℕ) (a : Fin 2) : R

The power xₖᵃ, for a bit a.

Equations

• S.xpow k a = if a = 0 then 1 else S.x k

noncomputable def MIPRE.PauliSites.unit {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) (a b : Fin 2) : R

The single-site matrix units xₖᵃ pₖ xₖᵇ.

Equations

• S.unit k a b = S.xpow k a * S.proj k * S.xpow k b

theorem MIPRE.PauliSites.proj_mul_self {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) : S.proj k * S.proj k = S.proj k

pₖ is idempotent.

theorem MIPRE.PauliSites.star_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) (k : ℕ) : star (S.proj k) = S.proj k

pₖ is self-adjoint.

theorem MIPRE.PauliSites.x_mul_proj_mul_x {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) : S.x k * S.proj k * S.x k = 1 - S.proj k

Conjugating by xₖ exchanges pₖ and 1 - pₖ.

theorem MIPRE.PauliSites.proj_mul_x_mul_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) : S.proj k * S.x k * S.proj k = 0

pₖ xₖ pₖ = 0.

theorem MIPRE.PauliSites.xpow_mul_self {R : Type u_1} [Ring R] [StarRing R] (S : PauliSites R) (k : ℕ) (a : Fin 2) : S.xpow k a * S.xpow k a = 1

(xₖᵃ)² = 1.

theorem MIPRE.PauliSites.xpow_mul_xpow_of_ne {R : Type u_1} [Ring R] [StarRing R] (S : PauliSites R) (k : ℕ) {a b : Fin 2} (h : a ≠ b) : S.xpow k a * S.xpow k b = S.x k

xₖᵃ xₖᵇ = xₖ for distinct bits.

theorem MIPRE.PauliSites.star_xpow {R : Type u_1} [Ring R] [StarRing R] (S : PauliSites R) (k : ℕ) (a : Fin 2) : star (S.xpow k a) = S.xpow k a

xₖᵃ is self-adjoint.

theorem MIPRE.PauliSites.unit_mul {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) (a b c d : Fin 2) : S.unit k a b * S.unit k c d = if b = c then S.unit k a d else 0

The multiplication rule of the single-site units.

theorem MIPRE.PauliSites.star_unit {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) (k : ℕ) (a b : Fin 2) : star (S.unit k a b) = S.unit k b a

The adjoint rule of the single-site units.

theorem MIPRE.PauliSites.sum_unit_diag {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (k : ℕ) : ∑ a : Fin 2, S.unit k a a = 1

The single-site units are unital: pₖ + xₖ pₖ xₖ = 1.

theorem MIPRE.PauliSites.isMatUnits_unit {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) (k : ℕ) : IsMatUnits (S.unit k)

The single-site units are unital 2 × 2 matrix units.

theorem MIPRE.PauliSites.commute_x_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) : Commute (S.x k) (S.proj l)

xₖ commutes with the projection at another site.

theorem MIPRE.PauliSites.commute_z_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) : Commute (S.z k) (S.proj l)

zₖ commutes with the projection at another site.

theorem MIPRE.PauliSites.commute_proj_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) : Commute (S.proj k) (S.proj l)

The projections at distinct sites commute.

theorem MIPRE.PauliSites.commute_xpow_xpow {R : Type u_1} [Ring R] [StarRing R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) (a b : Fin 2) : Commute (S.xpow k a) (S.xpow l b)

The powers of x at distinct sites commute.

theorem MIPRE.PauliSites.commute_xpow_proj {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) (a : Fin 2) : Commute (S.xpow k a) (S.proj l)

A power of xₖ commutes with the projection at another site.

theorem MIPRE.PauliSites.commute_unit {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) {k l : ℕ} (h : k ≠ l) (a b c d : Fin 2) : Commute (S.unit k a b) (S.unit l c d)

The single-site units at distinct sites commute.

noncomputable def MIPRE.PauliSites.units {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (n : ℕ) : (Fin n → Fin 2) → (Fin n → Fin 2) → R

The 2ⁿ × 2ⁿ matrix units on the sites 0, …, n - 1: e_{ij} = ∏ₖ unit k (iₖ) (jₖ), the bit at index 0 read at site n - 1.

Equations

• S.units 0 x_3 x_4 = 1
• S.units n.succ i j = S.unit n (i 0) (j 0) * S.units n (Fin.tail i) (Fin.tail j)

theorem MIPRE.PauliSites.commute_unit_units {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (n m : ℕ) : n ≤ m → ∀ (a b : Fin 2) (i j : Fin n → Fin 2), Commute (S.unit m a b) (S.units n i j)

A single-site unit at site m commutes with the units on the sites below n ≤ m.

theorem MIPRE.PauliSites.units_mul {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (n : ℕ) (i j k l : Fin n → Fin 2) : S.units n i j * S.units n k l = if j = k then S.units n i l else 0

The multiplication rule of the 2ⁿ × 2ⁿ units.

theorem MIPRE.PauliSites.star_units {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) (n : ℕ) (i j : Fin n → Fin 2) : star (S.units n i j) = S.units n j i

The adjoint rule of the 2ⁿ × 2ⁿ units.

theorem MIPRE.PauliSites.sum_units_diag {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] (S : PauliSites R) (n : ℕ) : ∑ i : Fin n → Fin 2, S.units n i i = 1

The 2ⁿ × 2ⁿ units are unital.

theorem MIPRE.PauliSites.isMatUnits_units {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) (n : ℕ) : IsMatUnits (S.units n)

The 2ⁿ × 2ⁿ units of Pauli sites are unital matrix units.

theorem MIPRE.PauliSites.hasDyadicUnits {R : Type u_1} [Ring R] [StarRing R] [Algebra ℂ R] [StarModule ℂ R] (S : PauliSites R) : HasDyadicUnits R

A ⋆-algebra with Pauli sites has unital dyadic matrix units (lem:pauli-sites-units).