The twisted Pauli algebra: a standard tracial algebra with unital dyadic matrix units

Work package T4 of C6b (planning/c6b-plan.md; reports/c6b-paper-proofs.md, §3.8). The value lemma's amplification (Theorems A and T of the report, §3) tensors a finite pair with a standard tracial algebra B whose ⋆-algebra B.A has unital 2ⁿ × 2ⁿ matrix units for every n (HasDyadicUnits, MIPRE/Foundations/MatUnits.lean). This file constructs one, the twisted Pauli algebra (pauliStd, pauliStd_hasDyadicUnits), in the interface CommutingRepetition.StdTracialAlgebra of the vendored commuting-repetition development.

• Labels and phase. The Pauli labels are Label = ℕ →₀ ZMod 2 × ZMod 2, a pair of bits (x, z) at each site. The phase is ω(g, h) = (-1)^{β(g, h)} with β(g, h) = ∑ᵢ z(g)ᵢ x(h)ᵢ, a bilinear, hence 2-cocycle, twist (phase_cocycle).
• The operators. On ℓ²(Label) the unitary W g sends δ_h to ω(g, h) δ_{g+h}, so that W g W h = ω(g, h) W (g + h) and (W g)⋆ = ω(g, g) W g.
• The algebra. pauliA is the linear span of the W g in B(ℓ²(Label)), a ⋆-subalgebra; it is not closed, which the interface does not ask for. The trace is the vector state at δ₀, tracial because τ(W g) = [g = 0]; the GNS map is a ↦ a δ₀, with dense range since its image contains every δ_g; the left action is the inclusion, and the right action is op a ↦ J a⋆ J for the antiunitary (J ξ)ₖ = ω(k, k) conj(ξₖ), which satisfies Tomita's identity J (a δ₀) = a⋆ δ₀ (J_pauliEmbed). That the two actions commute is checked on the dense range.
• The units. X_k = W (single k (1, 0)) and Z_k = W (single k (0, 1)) are Pauli sites in the sense of MIPRE.PauliSites (pauliSites), whose units Π_k X_kᵃ (1 + Z_k)/2 X_kᵇ are unital in pauliA itself, not only after the representation.

Names that would shadow the fields of StdTracialAlgebra are spelled out: the algebra is pauliA, its trace pauliTrace, the Hilbert space PauliSpace, the GNS map pauliEmbed and the right action pauliRight.

The interface imports all of Mathlib, but the file names the two Mathlib modules it needs, and compiles with only those: ℓ², and the C⋆-algebra of operators on a Hilbert space. The second is there for instance search rather than for a lemma: without it, Algebra ℂ B(ℓ²(Label)) and its scalar-tower instances are searched through the metric structure of the carrier of lp and run out of budget.

Pauli labels and the phase cocycle

@[reducible, inline]

abbrev MIPRE.Repetition.Pauli.Label : Type

Pauli labels: finitely supported sequences of pairs (x-bit, z-bit).

Equations

• MIPRE.Repetition.Pauli.Label = (ℕ →₀ ZMod 2 × ZMod 2)

def MIPRE.Repetition.Pauli.twist (g h : Label) : ZMod 2

The twist β(g, h) = ∑ᵢ z(g)ᵢ x(h)ᵢ, the half of the symplectic form that defines the phase.

Equations

• MIPRE.Repetition.Pauli.twist g h = Finsupp.sum g fun (i : ℕ) (a : ZMod 2 × ZMod 2) => a.2 * (h i).1

theorem MIPRE.Repetition.Pauli.twist_add_left (g g' h : Label) : twist (g + g') h = twist g h + twist g' h

The twist is additive in its first argument.

theorem MIPRE.Repetition.Pauli.twist_add_right (g h h' : Label) : twist g (h + h') = twist g h + twist g h'

The twist is additive in its second argument.

@[simp]

theorem MIPRE.Repetition.Pauli.twist_zero_left (h : Label) : twist 0 h = 0

β(0, h) = 0.

@[simp]

theorem MIPRE.Repetition.Pauli.twist_zero_right (g : Label) : twist g 0 = 0

β(g, 0) = 0.

theorem MIPRE.Repetition.Pauli.twist_single (k l : ℕ) (u v : ZMod 2 × ZMod 2) : (twist (fun₀ | k => u) fun₀ | l => v) = u.2 * if l = k then v.1 else 0

The twist of two single-site labels.

theorem MIPRE.Repetition.Pauli.label_add_self (g : Label) : g + g = 0

Every label is its own inverse.

def MIPRE.Repetition.Pauli.signChar (a : ZMod 2) : ℂ

The sign character ZMod 2 → {±1}.

Equations

• MIPRE.Repetition.Pauli.signChar a = if a = 0 then 1 else -1

@[simp]

theorem MIPRE.Repetition.Pauli.signChar_zero : signChar 0 = 1

(-1)⁰ = 1.

@[simp]

theorem MIPRE.Repetition.Pauli.signChar_one : signChar 1 = -1

(-1)¹ = -1.

theorem MIPRE.Repetition.Pauli.signChar_add (a b : ZMod 2) : signChar (a + b) = signChar a * signChar b

The sign character is a character.

theorem MIPRE.Repetition.Pauli.signChar_mul_self (a : ZMod 2) : signChar a * signChar a = 1

The sign character squares to 1.

theorem MIPRE.Repetition.Pauli.norm_signChar (a : ZMod 2) : ‖signChar a‖ = 1

The sign character is unimodular.

theorem MIPRE.Repetition.Pauli.conj_signChar (a : ZMod 2) : (starRingEnd ℂ) (signChar a) = signChar a

The sign character is real.

def MIPRE.Repetition.Pauli.phase (g h : Label) : ℂ

The phase ω(g, h) = (-1)^{β(g, h)}.

Equations

• MIPRE.Repetition.Pauli.phase g h = MIPRE.Repetition.Pauli.signChar (MIPRE.Repetition.Pauli.twist g h)

theorem MIPRE.Repetition.Pauli.phase_cocycle (g h k : Label) : phase g (k + g) * phase h (k + (g + h)) = phase g h * phase (g + h) (k + (g + h))

The cocycle identity of the phase, in the form W g W h = ω(g, h) W (g + h) needs at the coordinate k.

theorem MIPRE.Repetition.Pauli.norm_phase (g h : Label) : ‖phase g h‖ = 1

The phase is unimodular.

theorem MIPRE.Repetition.Pauli.phase_mul_self (g h : Label) : phase g h * phase g h = 1

The phase squares to 1.

theorem MIPRE.Repetition.Pauli.conj_phase (g h : Label) : (starRingEnd ℂ) (phase g h) = phase g h

The phase is real.

theorem MIPRE.Repetition.Pauli.phase_single (k l : ℕ) (u v : ZMod 2 × ZMod 2) : (phase (fun₀ | k => u) fun₀ | l => v) = signChar (u.2 * if l = k then v.1 else 0)

The phase of two single-site labels.

ℓ²(Label) and weighted permutations

@[reducible, inline]

abbrev MIPRE.Repetition.Pauli.PauliSpace : Type

The Hilbert space ℓ²(Label).

Equations

• MIPRE.Repetition.Pauli.PauliSpace = ↥(lp (fun (x : MIPRE.Repetition.Pauli.Label) => ℂ) 2)

def MIPRE.Repetition.Pauli.weightedPermFun (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) (ξ : PauliSpace) : PauliSpace

The vector k ↦ φ k * ξ (e k), for a unimodular weight φ and a permutation e.

Equations

• MIPRE.Repetition.Pauli.weightedPermFun e φ hφ ξ = ⟨fun (k : MIPRE.Repetition.Pauli.Label) => φ k * ↑ξ (e k), ⋯⟩

@[simp]

theorem MIPRE.Repetition.Pauli.weightedPermFun_apply (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) (ξ : PauliSpace) (k : Label) : ↑(weightedPermFun e φ hφ ξ) k = φ k * ↑ξ (e k)

The coordinates of a weighted permutation of a vector.

theorem MIPRE.Repetition.Pauli.norm_weightedPermFun (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) (ξ : PauliSpace) : ‖weightedPermFun e φ hφ ξ‖ = ‖ξ‖

A weighted permutation preserves the norm.

noncomputable def MIPRE.Repetition.Pauli.weightedPerm (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) : PauliSpace →L[ℂ] PauliSpace

A weighted permutation ξ ↦ (k ↦ φ k * ξ (e k)), as a bounded operator (an isometry).

Equations

• MIPRE.Repetition.Pauli.weightedPerm e φ hφ = { toFun := MIPRE.Repetition.Pauli.weightedPermFun e φ hφ, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

@[simp]

theorem MIPRE.Repetition.Pauli.weightedPerm_apply (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) (ξ : PauliSpace) (k : Label) : ↑((weightedPerm e φ hφ) ξ) k = φ k * ↑ξ (e k)

The coordinates of the image under a weighted permutation.

theorem MIPRE.Repetition.Pauli.norm_weightedPerm (e : Label ≃ Label) (φ : Label → ℂ) (hφ : ∀ (k : Label), ‖φ k‖ = 1) (ξ : PauliSpace) : ‖(weightedPerm e φ hφ) ξ‖ = ‖ξ‖

A weighted permutation is an isometry.

The twisted Pauli unitaries W g

noncomputable def MIPRE.Repetition.Pauli.W (g : Label) : PauliSpace →L[ℂ] PauliSpace

The twisted Pauli unitary W g, with W g δ_h = ω(g, h) δ_{g+h}.

Equations

• MIPRE.Repetition.Pauli.W g = MIPRE.Repetition.Pauli.weightedPerm (Equiv.addRight g) (fun (k : MIPRE.Repetition.Pauli.Label) => MIPRE.Repetition.Pauli.phase g (k + g)) ⋯

@[simp]

theorem MIPRE.Repetition.Pauli.W_apply (g : Label) (ξ : PauliSpace) (k : Label) : ↑((W g) ξ) k = phase g (k + g) * ↑ξ (k + g)

The coordinates of W g ξ: (W g ξ)ₖ = ω(g, k + g) ξ_{k+g}.

theorem MIPRE.Repetition.Pauli.norm_W (g : Label) (ξ : PauliSpace) : ‖(W g) ξ‖ = ‖ξ‖

W g is an isometry.

theorem MIPRE.Repetition.Pauli.W_mul (g h : Label) : W g * W h = phase g h • W (g + h)

W g W h = ω(g, h) W (g + h).

theorem MIPRE.Repetition.Pauli.W_zero : W 0 = 1

W 0 = 1.

theorem MIPRE.Repetition.Pauli.W_mul_self (g : Label) : W g * W g = phase g g • 1

(W g)² = ω(g, g).

theorem MIPRE.Repetition.Pauli.star_W (g : Label) : star (W g) = phase g g • W g

(W g)⋆ = ω(g, g) W g.

Basis vectors

noncomputable def MIPRE.Repetition.Pauli.basisVec (h : Label) : PauliSpace

The basis vector δ_h.

Equations

• MIPRE.Repetition.Pauli.basisVec h = lp.single 2 h 1

theorem MIPRE.Repetition.Pauli.basisVec_apply (h k : Label) : ↑(basisVec h) k = if k = h then 1 else 0

The coordinates of δ_h.

theorem MIPRE.Repetition.Pauli.W_basisVec (g h : Label) : (W g) (basisVec h) = phase g h • basisVec (g + h)

W g δ_h = ω(g, h) δ_{g+h}.

noncomputable def MIPRE.Repetition.Pauli.traceVec : PauliSpace

The trace vector δ₀.

Equations

• MIPRE.Repetition.Pauli.traceVec = MIPRE.Repetition.Pauli.basisVec 0

theorem MIPRE.Repetition.Pauli.W_traceVec (g : Label) : (W g) traceVec = basisVec g

W g δ₀ = δ_g.

theorem MIPRE.Repetition.Pauli.inner_traceVec_basisVec (h : Label) : inner ℂ traceVec (basisVec h) = if h = 0 then 1 else 0

⟪δ₀, δ_h⟫ = [h = 0].

The algebra

noncomputable def MIPRE.Repetition.Pauli.pauliSpan : Submodule ℂ (PauliSpace →L[ℂ] PauliSpace)

The linear span of the W g.

Equations

• MIPRE.Repetition.Pauli.pauliSpan = Submodule.span ℂ (Set.range MIPRE.Repetition.Pauli.W)

theorem MIPRE.Repetition.Pauli.W_mem_pauliSpan (g : Label) : W g ∈ pauliSpan

Each W g lies in the span.

theorem MIPRE.Repetition.Pauli.mul_mem_pauliSpan {a b : PauliSpace →L[ℂ] PauliSpace} (ha : a ∈ pauliSpan) (hb : b ∈ pauliSpan) : a * b ∈ pauliSpan

The span is closed under multiplication.

theorem MIPRE.Repetition.Pauli.star_mem_pauliSpan {a : PauliSpace →L[ℂ] PauliSpace} (ha : a ∈ pauliSpan) : star a ∈ pauliSpan

The span is closed under the adjoint.

def MIPRE.Repetition.Pauli.pauliA : StarSubalgebra ℂ (PauliSpace →L[ℂ] PauliSpace)

The twisted Pauli ⋆-algebra (lem:pauli-algebra): the linear span of the W g inside B(ℓ²(Label)).

Equations

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

theorem MIPRE.Repetition.Pauli.mem_pauliA {a : PauliSpace →L[ℂ] PauliSpace} : a ∈ pauliA ↔ a ∈ pauliSpan

Membership in pauliA is membership in the span.

noncomputable def MIPRE.Repetition.Pauli.w (g : Label) : ↥pauliA

W g as an element of pauliA.

Equations

• MIPRE.Repetition.Pauli.w g = ⟨MIPRE.Repetition.Pauli.W g, ⋯⟩

theorem MIPRE.Repetition.Pauli.w_zero : w 0 = 1

w 0 = 1.

theorem MIPRE.Repetition.Pauli.pauliA_induction {p : ↥pauliA → Prop} (hw : ∀ (g : Label), p (w g)) (h0 : p 0) (hadd : ∀ (a b : ↥pauliA), p a → p b → p (a + b)) (hsmul : ∀ (c : ℂ) (a : ↥pauliA), p a → p (c • a)) (a : ↥pauliA) : p a

Induction over the span, for elements of pauliA.

The trace and the GNS data

noncomputable def MIPRE.Repetition.Pauli.pauliTrace : ↥pauliA →ₗ[ℂ] ℂ

The trace of pauliA: the vector state at δ₀.

Equations

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

theorem MIPRE.Repetition.Pauli.pauliTrace_apply (a : ↥pauliA) : pauliTrace a = inner ℂ traceVec (↑a traceVec)

The trace is the vector state at δ₀.

theorem MIPRE.Repetition.Pauli.pauliTrace_one : pauliTrace 1 = 1

The trace is normalized.

theorem MIPRE.Repetition.Pauli.pauliTrace_star (a : ↥pauliA) : pauliTrace (star a) = star (pauliTrace a)

The trace commutes with the adjoint.

theorem MIPRE.Repetition.Pauli.pauliTrace_w_mul_comm (g h : Label) : pauliTrace (w g * w h) = pauliTrace (w h * w g)

The trace is tracial on the unitaries W g.

theorem MIPRE.Repetition.Pauli.pauliTrace_mul_comm (a b : ↥pauliA) : pauliTrace (a * b) = pauliTrace (b * a)

The trace is tracial.

noncomputable def MIPRE.Repetition.Pauli.pauliEmbed : ↥pauliA →ₗ[ℂ] PauliSpace

The GNS map a ↦ a δ₀.

Equations

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

theorem MIPRE.Repetition.Pauli.pauliEmbed_apply (a : ↥pauliA) : pauliEmbed a = ↑a traceVec

The GNS map is evaluation at δ₀.

theorem MIPRE.Repetition.Pauli.pauliEmbed_w (g : Label) : pauliEmbed (w g) = basisVec g

The GNS map sends w g to δ_g.

theorem MIPRE.Repetition.Pauli.inner_pauliEmbed (a b : ↥pauliA) : inner ℂ (pauliEmbed a) (pauliEmbed b) = pauliTrace (star a * b)

The GNS map realizes the trace: ⟪a δ₀, b δ₀⟫ = τ(a⋆ b).

theorem MIPRE.Repetition.Pauli.pauliEmbed_dense : DenseRange ⇑pauliEmbed

The GNS map has dense range: its image contains every δ_g.

theorem MIPRE.Repetition.Pauli.pauliEmbed_mul (a b : ↥pauliA) : pauliEmbed (a * b) = ↑a (pauliEmbed b)

The GNS map intertwines left multiplication with the operator.

The modular conjugation J and the right action

def MIPRE.Repetition.Pauli.J (ξ : PauliSpace) : PauliSpace

The modular conjugation (J ξ)ₖ = ω(k, k) conj(ξₖ): the antiunitary with J (a δ₀) = a⋆ δ₀.

Equations

• MIPRE.Repetition.Pauli.J ξ = ⟨fun (k : MIPRE.Repetition.Pauli.Label) => MIPRE.Repetition.Pauli.phase k k * (starRingEnd ((fun (x : MIPRE.Repetition.Pauli.Label) => ℂ) k)) (↑ξ k), ⋯⟩

@[simp]

theorem MIPRE.Repetition.Pauli.J_apply (ξ : PauliSpace) (k : Label) : ↑(J ξ) k = phase k k * (starRingEnd ((fun (x : Label) => ℂ) k)) (↑ξ k)

The coordinates of J ξ.

theorem MIPRE.Repetition.Pauli.J_add (ξ η : PauliSpace) : J (ξ + η) = J ξ + J η

J is additive.

theorem MIPRE.Repetition.Pauli.J_smul (c : ℂ) (ξ : PauliSpace) : J (c • ξ) = (starRingEnd ℂ) c • J ξ

J is conjugate-linear.

theorem MIPRE.Repetition.Pauli.J_J (ξ : PauliSpace) : J (J ξ) = ξ

J is an involution.

theorem MIPRE.Repetition.Pauli.norm_J (ξ : PauliSpace) : ‖J ξ‖ = ‖ξ‖

J is isometric.

theorem MIPRE.Repetition.Pauli.inner_J_J (ξ η : PauliSpace) : inner ℂ (J ξ) (J η) = inner ℂ η ξ

J is antiunitary: ⟪J ξ, J η⟫ = ⟪η, ξ⟫.

theorem MIPRE.Repetition.Pauli.inner_J_left (u v : PauliSpace) : inner ℂ (J u) v = inner ℂ (J v) u

⟪J u, v⟫ = ⟪J v, u⟫.

noncomputable def MIPRE.Repetition.Pauli.conjJ (T : PauliSpace →L[ℂ] PauliSpace) : PauliSpace →L[ℂ] PauliSpace

Conjugation by J: T ↦ J T J, a complex-antilinear ⋆-preserving ring map.

Equations

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

@[simp]

theorem MIPRE.Repetition.Pauli.conjJ_apply (T : PauliSpace →L[ℂ] PauliSpace) (ξ : PauliSpace) : (conjJ T) ξ = J (T (J ξ))

(J T J) ξ = J (T (J ξ)).

theorem MIPRE.Repetition.Pauli.conjJ_mul (S T : PauliSpace →L[ℂ] PauliSpace) : conjJ (S * T) = conjJ S * conjJ T

Conjugation by J is multiplicative.

theorem MIPRE.Repetition.Pauli.conjJ_one : conjJ 1 = 1

Conjugation by J is unital.

theorem MIPRE.Repetition.Pauli.conjJ_add (S T : PauliSpace →L[ℂ] PauliSpace) : conjJ (S + T) = conjJ S + conjJ T

Conjugation by J is additive.

theorem MIPRE.Repetition.Pauli.conjJ_smul (c : ℂ) (T : PauliSpace →L[ℂ] PauliSpace) : conjJ (c • T) = (starRingEnd ℂ) c • conjJ T

Conjugation by J is conjugate-linear.

theorem MIPRE.Repetition.Pauli.conjJ_zero : conjJ 0 = 0

Conjugation by J sends 0 to 0.

theorem MIPRE.Repetition.Pauli.conjJ_star (T : PauliSpace →L[ℂ] PauliSpace) : conjJ (star T) = star (conjJ T)

Conjugation by J commutes with the adjoint.

theorem MIPRE.Repetition.Pauli.J_basisVec (g : Label) : J (basisVec g) = phase g g • basisVec g

J δ_g = ω(g, g) δ_g.

theorem MIPRE.Repetition.Pauli.J_pauliEmbed (a : ↥pauliA) : J (pauliEmbed a) = pauliEmbed (star a)

Tomita's identity on pauliA: J (a δ₀) = a⋆ δ₀.

noncomputable def MIPRE.Repetition.Pauli.pauliRight : (↥pauliA)ᵐᵒᵖ →⋆ₐ[ℂ] PauliSpace →L[ℂ] PauliSpace

The right action of pauliA: op a ↦ J a⋆ J.

Equations

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

theorem MIPRE.Repetition.Pauli.pauliRight_op (a : ↥pauliA) : pauliRight (MulOpposite.op a) = conjJ (star ↑a)

The right action of op a is J a⋆ J.

theorem MIPRE.Repetition.Pauli.pauliRight_pauliEmbed (a b : ↥pauliA) : (pauliRight (MulOpposite.op a)) (pauliEmbed b) = pauliEmbed (b * a)

The right action multiplies on the right: R(op a) (b δ₀) = (b a) δ₀.

theorem MIPRE.Repetition.Pauli.pauliA_commute_pauliRight (a b : ↥pauliA) : Commute (pauliA.subtype a) (pauliRight (MulOpposite.op b))

The left and right actions commute, checked on the dense range of the GNS map.

noncomputable def MIPRE.Repetition.Pauli.pauliStd : CommutingRepetition.StdTracialAlgebra

The twisted Pauli algebra as a standard tracial algebra (lem:pauli-algebra): pauliA with the vector trace at δ₀, on ℓ²(Label), acting on the left by inclusion and on the right through J.

Equations

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

The Pauli sites and the dyadic units

noncomputable def MIPRE.Repetition.Pauli.xLabel (k : ℕ) : Label

The label of X at site k.

Equations

• MIPRE.Repetition.Pauli.xLabel k = fun₀ | k => (1, 0)

noncomputable def MIPRE.Repetition.Pauli.zLabel (k : ℕ) : Label

The label of Z at site k.

Equations

• MIPRE.Repetition.Pauli.zLabel k = fun₀ | k => (0, 1)

theorem MIPRE.Repetition.Pauli.phase_xLabel_left (k : ℕ) (h : Label) : phase (xLabel k) h = 1

The X labels carry no z-bits, so their phase on the left is trivial.

theorem MIPRE.Repetition.Pauli.phase_zLabel_right (g : Label) (l : ℕ) : phase g (zLabel l) = 1

The Z labels carry no x-bits, so their phase on the right is trivial.

theorem MIPRE.Repetition.Pauli.phase_zLabel_xLabel (k l : ℕ) : phase (zLabel k) (xLabel l) = if l = k then -1 else 1

Z_k and X_l anticommute exactly when k = l.

theorem MIPRE.Repetition.Pauli.w_mul_of_phase_eq_one {g h : Label} (hgh : phase g h = 1) : w g * w h = w (g + h)

w g w h = w (g + h) when the phase is trivial. The three w-lemmas below are proved in the operators, where the scalar actions are found much faster than on the subalgebra.

theorem MIPRE.Repetition.Pauli.w_mul_of_phase_eq_neg_one {g h : Label} (hgh : phase g h = -1) : w g * w h = -w (g + h)

w g w h = -w (g + h) when the phase is -1.

theorem MIPRE.Repetition.Pauli.star_w_of_phase_eq_one {g : Label} (hg : phase g g = 1) : star (w g) = w g

w g is self-adjoint when ω(g, g) = 1.

noncomputable def MIPRE.Repetition.Pauli.pauliSites : PauliSites ↥pauliA

The Pauli sites of pauliA: x k = W (X_k), z k = W (Z_k).

Equations

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

theorem MIPRE.Repetition.Pauli.pauliStd_hasDyadicUnits : HasDyadicUnits pauliStd.A

The twisted Pauli algebra has unital dyadic matrix units (lem:pauli-algebra), in pauliStd.A itself: the units of its Pauli sites (MIPRE.PauliSites.hasDyadicUnits).