The Pauli rotation branching rule, with its case split closed

Rotation.lean proves the two branches of apd:eq:pauli_rotation_branch over an abstract ℂ-algebra: rot_conj_of_commute for a commuting generator, rot_conj_of_anticommute for an anticommuting one. What it cannot see is that those two branches exhaust the cases: in an abstract algebra a pair G, P need neither commute nor anticommute. This file specializes the rule to Pauli strings, where the dichotomy is a theorem, and states the rule as a single identity whose branch is decided by the symplectic form.

PauliString.toMatrix_commute_or_anticommute supplies the dichotomy, PauliString.isSelfAdjoint_iff_mul_self_eq_one supplies both rot_* hypotheses from one, and pauli_rotation_branch is then the paper's equation with an if, not a hypothesis, deciding the branch.

Main results

• rot_toMatrix_mem_unitary: a rotation generated by a Hermitian Pauli string is unitary.
• pauli_rotation_branch: apd:eq:pauli_rotation_branch for Pauli strings, the branch being selected by sympForm G s.
• pauli_rotation_branch_commute, pauli_rotation_branch_anticommute: the two branches separately.
• pauli_rotation_branch_anticommute_hermitian: the anticommuting branch with the real coefficient sin θ on the Hermitian partner i G s.
• pauli_rotation_branch_anticommute_bounds: the anticommuting branch together with the two-sided weight bound and the non-collinearity of the two terms.

The three consequences of the identity

The paper draws three consequences from the identity: (1) the transition is sparse in the Pauli basis, (2) the weight change is bounded by the locality of G, and (3) the amplitude of the new term is damped by sin(dt). Rotation.lean delivers the arithmetic under (1) and (3) over an abstract algebra. pauli_rotation_branch_anticommute_bounds collects what holds at the level of Pauli operators: (2) in full and the non-degeneracy half of (3). The statements about coefficients in the Pauli basis live in Pauli/Coeff.lean and Pauli/Flow.lean.

1. Sparsity. The image is a ℂ-combination of at most two Pauli operators, s and G s ("at most", since the second coefficient vanishes at θ = 0 and the first at θ = π/2). Sparsity in the Pauli basis is a statement about a coefficient vector, and no basis is built in this file: it needs the orthogonality relation Tr(s s') = δ of def:pauli_basis (Pauli/Trace.lean), and the coefficient-level form of the rule is coeffVec_conj in Pauli/Flow.lean. "Two terms of the Pauli group" is strictly weaker than "two non-zero coefficients in the Pauli basis", and it is the former that is proved here.
2. Weight. |s| - (k_h - 1) ≤ |G s| ≤ |s| + (k_h - 1) for |G| ≤ k_h, from Pauli/Weight.lean, proved in both directions.
3. Damping. The second term's coefficient is i sin(θ), and the two terms are non-collinear (toMatrix_mul_ne_smul), so the decomposition is non-degenerate and that coefficient is not a rescaling of the first term. Rotation.lean records that distinctness is not enough for this, by the pair G = Z, P = E₁₀ in Matrix (Fin 2) (Fin 2) ℂ, for which both rotation hypotheses hold and G * P = -P. No Pauli string can play that role. The damping of the coefficient in the Pauli basis needs the basis and is part of the norm flow in Pauli/Flow.lean.

Scope

The sin(dt) factor being small is a statement about dt, not about Paulis, and belongs to the ladder (Lean4LPD.Ladder). Orthogonality of the Pauli operators is in Pauli/Trace.lean, the coefficient vector in Pauli/Coeff.lean, and the orthogonality of conjugation acting on it, used in the proof of apd:thm:local_flow_k_local, is norm_rotAct in Pauli/Flow.lean.

The theorems below are stated for the closed form rot G θ and for the entrywise matrix toMatrix. That rot (toMatrix G) θ is the matrix exponential exp(i G θ/2) is rot_toMatrix_eq_exp in RotationExp.lean. That toMatrix s is a fourth root of unity times the tensor product P₁ ⊗ ⋯ ⊗ Pₙ of one-qubit Pauli matrices is toMatrix_eq_phase_tensor in Pauli/Tensor.lean; the one-qubit case is also checked entry by entry in Pauli/Matrix.lean.

theorem Lean4LPD.PauliString.rot_toMatrix_mem_unitary {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (θ : ℝ) : rot G.toMatrix θ ∈ unitary (Matrix (Bits n) (Bits n) ℂ)

Rotations generated by a Hermitian Pauli string are unitary, so any product of them is — including the product U_g = ∏_{l ≤ g} e^{-i G_l dt/2} of apd:thm:local_flow_k_local. That is the whole prefix of the trajectory, not a layer: a layer V_γ in the sense of apd:thm:layer_inflow carries the extra hypothesis of pairwise disjoint supports and is treated in Pauli/LayerFlow.lean.

In this file's convention U_g is ∏ rot G_l (-dt), not ∏ rot G_l dt, since rot G θ is the + exponential (Rotation.lean's Conventions block). This is Lean4LPD.rot_mem_unitary with both of its hypotheses discharged from the single hypothesis IsSelfAdjoint G.

theorem Lean4LPD.PauliString.pauli_rotation_branch {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (s : PauliString n) (θ : ℝ) : rot G.toMatrix θ * s.toMatrix * rot G.toMatrix (-θ) = if G.sympForm s = 0 then s.toMatrix else ↑(Real.cos θ) • s.toMatrix + (Complex.I * ↑(Real.sin θ)) • (G * s).toMatrix

apd:eq:pauli_rotation_branch, for Pauli strings, with the case split closed.

e^{i G dt/2} s e^{-i G dt/2} = s if ⟪G,s⟫ = 0, e^{i G dt/2} s e^{-i G dt/2} = cos(dt) s + i sin(dt) · G s if ⟪G,s⟫ = 1.

The paper states the rule as two cases, [G,P] = 0 and {G,P} = 0. Here the branch is selected by sympForm G s, which takes only the values 0 and 1 (sympForm_eq_zero_or_one) — so the if is total and the two branches really are all of them. That is the difference between this statement and Lean4LPD.rot_conj_of_commute / rot_conj_of_anticommute, which are conditioned on hypotheses that over an abstract algebra are not exhaustive. That the branch condition is the paper's condition, and not merely a sufficient one, is toMatrix_commute_iff and toMatrix_anticommute_iff — iffs at the level of operators, so sympForm G s = 0 holds exactly when [G,P] = 0 does.

The left-hand side is written with rot, the closed form. By rot_toMatrix_eq_exp and rot_toMatrix_neg_eq_exp in RotationExp.lean the two factors are the matrix exponentials exp(i G θ/2) and exp(-i G θ/2), so this is the paper's equation and not only a closed-form analogue of it.

The only hypothesis is IsSelfAdjoint G, which by isSelfAdjoint_iff_mul_self_eq_one also supplies the G * G = 1 that both rot_* lemmas need. Note θ is the paper's conjugation angle dt, following Rotation.lean's convention: a physical rotation e^{-i α_l G_l τ} has dt = 2 α_l τ.

theorem Lean4LPD.PauliString.pauli_rotation_branch_commute {n : ℕ} {G s : PauliString n} (hG : IsSelfAdjoint G) (h : G.sympForm s = 0) (θ : ℝ) : rot G.toMatrix θ * s.toMatrix * rot G.toMatrix (-θ) = s.toMatrix

The commuting branch: if ⟪G,s⟫ = 0, no rotation occurs and the Pauli operator is unchanged; in particular its weight does not change.

theorem Lean4LPD.PauliString.pauli_rotation_branch_anticommute {n : ℕ} {G s : PauliString n} (hG : IsSelfAdjoint G) (h : G.sympForm s = 1) (θ : ℝ) : rot G.toMatrix θ * s.toMatrix * rot G.toMatrix (-θ) = ↑(Real.cos θ) • s.toMatrix + (Complex.I * ↑(Real.sin θ)) • (G * s).toMatrix

The anticommuting branch: if ⟪G,s⟫ = 1, the image has two terms, the new one G s carrying i sin(θ).

theorem Lean4LPD.PauliString.pauli_rotation_branch_anticommute_hermitian {n : ℕ} {G s : PauliString n} (hG : IsSelfAdjoint G) (h : G.sympForm s = 1) (θ : ℝ) : rot G.toMatrix θ * s.toMatrix * rot G.toMatrix (-θ) = ↑(Real.cos θ) • s.toMatrix + ↑(Real.sin θ) • (phaseMul 1 (G * s)).toMatrix

The anticommuting branch in the variables of the norm-flow proof: a real coefficient on a Hermitian partner.

The proof of apd:thm:local_flow_k_local treats conjugation as a real orthogonal matrix acting on the coefficient vector in the Pauli basis: the Paulis anticommuting with the generator are paired as s ↔ ±i G_g s, and each pair undergoes a planar rotation by the angle dt. pauli_rotation_branch_anticommute above is not yet in that form: it carries the complex coefficient i sin θ on G s, and G s is anti-Hermitian when G and s anticommute. Absorbing the i into the operator fixes both at once — i G s is Hermitian (isSelfAdjoint_phaseMul_one_mul) and the coefficient becomes the real sin θ.

This is the form consumed by the coefficient-vector computation coeff_conj in Pauli/Flow.lean, and the reason isSelfAdjoint_phaseMul_one_mul and weight_sub_le_weight_phaseMul_one_mul are stated about the partner rather than the bare product.

theorem Lean4LPD.PauliString.pauli_rotation_branch_anticommute_bounds {n : ℕ} {G s : PauliString n} {kh : ℕ} (hG : IsSelfAdjoint G) (h : G.sympForm s = 1) (hk : G.weight ≤ kh) (θ : ℝ) : rot G.toMatrix θ * s.toMatrix * rot G.toMatrix (-θ) = ↑(Real.cos θ) • s.toMatrix + (Complex.I * ↑(Real.sin θ)) • (G * s).toMatrix ∧ s.weight - (kh - 1) ≤ (G * s).weight ∧ (G * s).weight ≤ s.weight + (kh - 1) ∧ ∀ (c : ℂ), (G * s).toMatrix ≠ c • s.toMatrix

The anticommuting branch with the bounds that go with it, for a k_h-local generator.

The conjuncts are, in order: the identity; the two halves of the weight bound; and the non-collinearity of the two terms.

Measured against the three consequences the paper draws from apd:eq:pauli_rotation_branch, that is consequence (2), the weight bound, in full, the non-degeneracy half of (3) — the i sin(θ) coefficient is not a rescaling of the first term — and none of (1), which is a statement about coefficients in the Pauli basis and needs a basis that this file does not build (see the module docstring). The subtraction weight s - (kh - 1) is truncated subtraction in ℕ; that is harmless, since when it truncates to 0 the lower bound holds trivially.

Stated as one theorem because the paper states one equation with one set of consequences, and because a reader checking the correspondence should not have to assemble it.