The layer light cone of a Trotter step

This file formalizes the weight part of the light-cone lemma apd:thm:lightcone. A layer of k_h-local Pauli rotations with pairwise disjoint supports multiplies the weight of a Pauli string by at most k_h (layer_weight_le), so a sequence of L such layers multiplies it by at most k_h ^ L (reachable_weight_le). One step of the pth-order product formula apd:eq:suzuki consists of ΥΓ layers, where Γ is the number of disjoint-support groups H_γ of the Hamiltonian and Υ = 2·5^{p/2−1} is the depth overhead of the formula, and the input of a step has weight at most w* after the preceding truncation. This is the count behind the weight bound w* k_h^{ΥΓ} on the Pauli strings of the discarded component Õ^{(d)}_{≥w*+1} of apd:eq:step_component. An explicit 8-qubit brickwork with k_h = 2 shows that the bound is attained after two layers, and that in a second-order step a string is reachable whose weight exceeds w* k_h^Γ: the exponent has to count the ΥΓ layers of a step and not the Γ groups.

Main definitions

• PauliString.branch G p: the Pauli strings that can appear when p is conjugated by a rotation generated by G, namely p and, when G and p anticommute, the partner i G p.
• PauliString.oneLayer L p, PauliString.reachable Ls p: the same for a layer L of generators and for a list Ls of layers.
• PauliString.IsLayer kh L: the generators in L have pairwise disjoint supports and weight at most kh. This is also the layer hypothesis of Pauli/LayerFlow.lean and the files built on it.
• PauliString.hitting L S, PauliString.cover L S: the generators of L whose support meets a set S of qubits, and the one-layer light cone of S.
• LayerWitness.L₁, LayerWitness.L₂: the two layers of an 8-qubit brickwork with k_h = 2; LayerWitness.P₄, LayerWitness.P₆: Hermitian Pauli strings of weight 4 and 6.

Main results

• PauliString.sympForm_eq_zero_of_disjoint_support: Pauli strings with disjoint supports commute.
• PauliString.support_subset_cover, PauliString.card_cover_le: everything one layer reaches from p is supported in cover L (support p), and (cover L S).card ≤ kh * S.card.
• PauliString.layer_weight_le: q ∈ oneLayer L p → weight q ≤ kh * weight p.
• PauliString.reachable_weight_le: q ∈ reachable Ls p → weight q ≤ kh ^ Ls.length * weight p.
• LayerWitness.gamma_layers_weight_le, LayerWitness.gamma_layers_weight_four: from the weight-one input Z₃, the largest weight reachable in the two layers [L₁, L₂] is exactly 4 = w* k_h^2, so the bound of reachable_weight_le is attained there.
• LayerWitness.gamma_weight_bound_false, LayerWitness.gamma_weight_bound_false_unmerged: in the layer sequence of a second-order step, [L₁, L₂, L₁] or [L₁, L₂, L₂, L₁] with Γ = 2, the string P₆ of weight 6 > 4 = w* k_h^Γ is reachable. Pauli/LayerCounterexample.lean upgrades this from reachability to a nonzero coefficient of the discarded operator, which shows that the exponent ΥΓ cannot be replaced by Γ.

Layers and reachable sets

A layer is a list of Pauli generators with pairwise disjoint supports, each of weight at most k_h (IsLayer), as in the hypothesis of apd:thm:lightcone. A k_h-local Pauli rotation generated by G, acting on a Pauli string p, either leaves it alone or splits it in two, according to whether G and p commute (commute_or_anticommute in Pauli/Basic.lean); branch is that two-way split, oneLayer composes it across a layer, and reachable across a list of layers.

reachable is defined combinatorially: it records which strings can appear under the branching rule apd:eq:pauli_rotation_branch and ignores the rotation angles. It therefore over-approximates the support of the conjugated operator and is not a certificate that any coefficient is nonzero. A containing set is exactly what an upper bound on the weight needs. In the other direction, a heavy element of reachable does not by itself show that the conjugated operator has a heavy Pauli component, because particular angles or cancellations between branches can make a coefficient vanish. Pauli/LayerCounterexample.lean supplies that step for the second-order word: it computes the coefficient of P₆ in closed form, shows that it is nonzero at every small angle, and shows that it survives in the discarded operator.

Why the per-layer factor is k_h

layer_weight_le and its iterate reachable_weight_le are stated for a general layer. The proof is a light-cone count: at most |p| generators of the layer can branch, because a generator that anticommutes with p must overlap its support (sympForm_eq_zero_of_disjoint_support) and the layer's supports are disjoint; each contributes at most k_h sites, and each of them consumes at least one site of p. That is where the sharp factor k_h comes from rather than k_h + 1.

Support arithmetic

Small facts about support that Pauli/Weight.lean does not need but the light-cone count does.

theorem Lean4LPD.PauliString.support_mul_subset {n : ℕ} (s t : PauliString n) : (s * t).support ⊆ s.support ∪ t.support

The support of a product is contained in the union of the supports.

@[simp]

theorem Lean4LPD.PauliString.support_phaseMul {n : ℕ} (k : ZMod 4) (s : PauliString n) : (phaseMul k s).support = s.support

The support does not see the phase — the Finset refinement of weight_phaseMul.

theorem Lean4LPD.PauliString.antiSites_subset_inter {n : ℕ} (G s : PauliString n) : G.antiSites s ⊆ G.support ∩ s.support

A locally anticommuting site lies in both supports.

theorem Lean4LPD.PauliString.sympForm_eq_zero_of_disjoint_support {n : ℕ} {G p : PauliString n} (h : Disjoint G.support p.support) : G.sympForm p = 0

Pauli strings with disjoint supports commute. This is what makes a layer a layer: the generators of one disjoint-support layer of apd:thm:lightcone commute with each other, so the layer is a product of commuting Pauli rotations.

theorem Lean4LPD.PauliString.inter_support_nonempty_of_sympForm {n : ℕ} {G p : PauliString n} (h : G.sympForm p = 1) : (G.support ∩ p.support).Nonempty

Contrapositive of the previous theorem, in the form the light-cone count consumes: a generator that anticommutes with p must touch p.

The branching process

One Pauli rotation, one layer, a list of layers. Every set here is a Finset, so the witness at the end of the file is a finite computation.

def Lean4LPD.PauliString.branch {n : ℕ} (G p : PauliString n) : Finset (PauliString n)

The two branches of one k_h-local Pauli rotation. Conjugating p by the rotation generated by G, with conjugation angle θ, leaves p alone when G and p commute and produces cos θ · p + sin θ · (i G p) when they anticommute (apd:eq:pauli_rotation_branch, formalized as pauli_rotation_branch), so the Pauli strings that can appear are p and, in the anticommuting case, the partner i G p.

This is a statement about which strings can appear, not about their coefficients: branch ignores the angle, so it over-approximates the support of the conjugated operator at any particular θ. That is the right side to err on for an upper bound on the weight.

Equations

• G.branch p = if G.sympForm p = 1 then {p, Lean4LPD.PauliString.phaseMul 1 (G * p)} else {p}

@[simp]

theorem Lean4LPD.PauliString.self_mem_branch {n : ℕ} (G p : PauliString n) : p ∈ G.branch p

theorem Lean4LPD.PauliString.partner_mem_branch {n : ℕ} {G p : PauliString n} (h : G.sympForm p = 1) : phaseMul 1 (G * p) ∈ G.branch p

The anticommuting branch: the partner i G p is reachable.

theorem Lean4LPD.PauliString.support_subset_of_mem_branch {n : ℕ} {G p q : PauliString n} (hq : q ∈ G.branch p) : q.support ⊆ p.support ∪ G.support

def Lean4LPD.PauliString.oneLayer {n : ℕ} (L : List (PauliString n)) (p : PauliString n) : Finset (PauliString n)

One layer, applied generator by generator. The generators of a layer have disjoint supports and so commute, which is why the order in the list is immaterial to the result and why branch's test can be read off the string entering the layer.

Equations

• Lean4LPD.PauliString.oneLayer [] x✝ = {x✝}
• Lean4LPD.PauliString.oneLayer (G :: Gs) x✝ = (G.branch x✝).biUnion (Lean4LPD.PauliString.oneLayer Gs)

@[simp]

theorem Lean4LPD.PauliString.oneLayer_nil {n : ℕ} (p : PauliString n) : oneLayer [] p = {p}

@[simp]

theorem Lean4LPD.PauliString.oneLayer_cons {n : ℕ} (G : PauliString n) (Gs : List (PauliString n)) (p : PauliString n) : oneLayer (G :: Gs) p = (G.branch p).biUnion (oneLayer Gs)

def Lean4LPD.PauliString.reachable {n : ℕ} (layers : List (List (PauliString n))) (p : PauliString n) : Finset (PauliString n)

A sequence of layers, applied one after another, the head of the list first. One Trotter step of the pth-order product formula apd:eq:suzuki is a sequence of ΥΓ layers.

Equations

• Lean4LPD.PauliString.reachable [] x✝ = {x✝}
• Lean4LPD.PauliString.reachable (L :: Ls) x✝ = (Lean4LPD.PauliString.oneLayer L x✝).biUnion (Lean4LPD.PauliString.reachable Ls)

@[simp]

theorem Lean4LPD.PauliString.reachable_nil {n : ℕ} (p : PauliString n) : reachable [] p = {p}

@[simp]

theorem Lean4LPD.PauliString.reachable_cons {n : ℕ} (L : List (PauliString n)) (Ls : List (List (PauliString n))) (p : PauliString n) : reachable (L :: Ls) p = (oneLayer L p).biUnion (reachable Ls)

theorem Lean4LPD.PauliString.self_mem_oneLayer {n : ℕ} (L : List (PauliString n)) (p : PauliString n) : p ∈ oneLayer L p

A string can always sit out a layer: every generator's branch retains its input, so p itself survives the whole layer unbranched.

theorem Lean4LPD.PauliString.reachable_subset_cons {n : ℕ} (L : List (PauliString n)) (Ls : List (List (PauliString n))) (p : PauliString n) : reachable Ls p ⊆ reachable (L :: Ls) p

Inserting a layer only enlarges the reachable set, by self_mem_oneLayer.

theorem Lean4LPD.PauliString.reachable_subset_reachable_cons {n : ℕ} {Ls Ls' : List (List (PauliString n))} (h : ∀ (r : PauliString n), reachable Ls r ⊆ reachable Ls' r) (L : List (PauliString n)) (p : PauliString n) : reachable (L :: Ls) p ⊆ reachable (L :: Ls') p

Enlarging the reachable set of a suffix enlarges it for the whole sequence: the two sequences run the same head layer and only then differ.

structure Lean4LPD.PauliString.IsLayer {n : ℕ} (kh : ℕ) (L : List (PauliString n)) : Prop

A layer of k_h-local rotations with disjoint supports: the hypothesis that apd:thm:lightcone places on each layer of a Trotter step.

• disjoint : List.Pairwise (fun (G H : PauliString n) => Disjoint G.support H.support) L

  Distinct generators of the layer act on disjoint sets of qubits.

• weight_le (G : PauliString n) : G ∈ L → G.weight ≤ kh

  Every generator is k_h-local.

theorem Lean4LPD.PauliString.IsLayer.disjoint_of_mem {n kh : ℕ} {G H : PauliString n} {L : List (PauliString n)} (hL : IsLayer kh L) (hG : G ∈ L) (hH : H ∈ L) (hne : G ≠ H) : Disjoint G.support H.support

Disjointness in the pointwise form the count needs. Stated separately because List.Pairwise orders its pairs and Disjoint does not care.

The light cone of one layer

cover L S is the set of qubits a string supported in S can reach through one layer: S itself, together with the full support of every generator that touches S. The two lemmas below are the two halves of the per-layer weight bound: containment, then the count.

def Lean4LPD.PauliString.hitting {n : ℕ} (L : List (PauliString n)) (S : Finset (Fin n)) : Finset (PauliString n)

The generators of L whose support meets S. Only these can branch.

Equations

• Lean4LPD.PauliString.hitting L S = {G ∈ L.toFinset | (G.support ∩ S).Nonempty}

theorem Lean4LPD.PauliString.mem_hitting {n : ℕ} {G : PauliString n} {L : List (PauliString n)} {S : Finset (Fin n)} : G ∈ hitting L S ↔ G ∈ L ∧ (G.support ∩ S).Nonempty

def Lean4LPD.PauliString.cover {n : ℕ} (L : List (PauliString n)) (S : Finset (Fin n)) : Finset (Fin n)

The one-layer light cone of a set of qubits.

Equations

• Lean4LPD.PauliString.cover L S = S ∪ (Lean4LPD.PauliString.hitting L S).biUnion Lean4LPD.PauliString.support

@[simp]

theorem Lean4LPD.PauliString.cover_nil {n : ℕ} (S : Finset (Fin n)) : cover [] S = S

theorem Lean4LPD.PauliString.subset_cover {n : ℕ} (L : List (PauliString n)) (S : Finset (Fin n)) : S ⊆ cover L S

theorem Lean4LPD.PauliString.support_subset_cover_of_mem_hitting {n : ℕ} {G : PauliString n} {L : List (PauliString n)} {S : Finset (Fin n)} (h : G ∈ hitting L S) : G.support ⊆ cover L S

theorem Lean4LPD.PauliString.hitting_subset_cons {n : ℕ} (G : PauliString n) (Gs : List (PauliString n)) (S : Finset (Fin n)) : hitting Gs S ⊆ hitting (G :: Gs) S

theorem Lean4LPD.PauliString.cover_subset_cons {n : ℕ} (G : PauliString n) (Gs : List (PauliString n)) (S : Finset (Fin n)) : cover Gs S ⊆ cover (G :: Gs) S

theorem Lean4LPD.PauliString.cover_subset_cover_cons {n : ℕ} {S T : Finset (Fin n)} {G : PauliString n} {Gs : List (PauliString n)} (hG : ∀ H ∈ Gs, Disjoint G.support H.support) (hGS : (G.support ∩ S).Nonempty) (hT : T ⊆ S ∪ G.support) : cover Gs T ⊆ cover (G :: Gs) S

The step of the containment induction: once the head generator G has fired, the strings it produces are supported in S ∪ supp G, and — because the rest of the layer is disjoint from G — the remaining generators that can still fire are exactly those that could already fire from S. So the light cone does not compound within a layer.

theorem Lean4LPD.PauliString.support_subset_cover {n : ℕ} {L : List (PauliString n)} : List.Pairwise (fun (G H : PauliString n) => Disjoint G.support H.support) L → ∀ {p q : PauliString n}, q ∈ oneLayer L p → q.support ⊆ cover L p.support

Containment. Everything one layer can reach from p is supported in the light cone of supp p.

theorem Lean4LPD.PauliString.card_cover_le {n kh : ℕ} {L : List (PauliString n)} (hL : IsLayer kh L) (hkh : 1 ≤ kh) (S : Finset (Fin n)) : (cover L S).card ≤ kh * S.card

The count. A layer of k_h-local generators with disjoint supports has a light cone at most k_h times as large as the set it starts from.

The factor is k_h and not k_h + 1 because each firing generator pays for itself out of S: its support meets S, the supports are disjoint, so the firing generators inject into S ∩ U, and the part of S no generator touches is carried along unchanged.

theorem Lean4LPD.PauliString.layer_weight_le {n kh : ℕ} {p q : PauliString n} {L : List (PauliString n)} (hL : IsLayer kh L) (hkh : 1 ≤ kh) (hq : q ∈ oneLayer L p) : q.weight ≤ kh * p.weight

One layer multiplies the Pauli weight by at most k_h. This is the per-layer step in the proof of apd:thm:lightcone, obtained by combining the containment support_subset_cover with the count card_cover_le.

theorem Lean4LPD.PauliString.reachable_weight_le {n kh : ℕ} {Ls : List (List (PauliString n))} : (∀ L ∈ Ls, IsLayer kh L) → 1 ≤ kh → ∀ {p q : PauliString n}, q ∈ reachable Ls p → q.weight ≤ kh ^ Ls.length * p.weight

The L-fold iterate, |q| ≤ k_h^L |p| after L layers.

With |p| ≤ w* and L = ΥΓ, the number of layers of one Trotter step of the pth-order formula apd:eq:suzuki, the right-hand side is at most w* k_h^{ΥΓ}, the weight bound of apd:thm:lightcone for the Pauli strings of the discarded component apd:eq:step_component. Nothing is assumed about how the layers are related: they may repeat, as they do in a second-order step.

Single-site Pauli strings

Enough notation to write a concrete brickwork down. Both carry phase 0, which is the Hermitian choice for a string with no Y site (isSelfAdjoint_iff_phase).

def Lean4LPD.PauliString.X {n : ℕ} (i : Fin n) : PauliString n

The single-site X_i.

Equations

• Lean4LPD.PauliString.X i = { x := fun (j : Fin n) => if j = i then 1 else 0, z := 0, phase := 0 }

def Lean4LPD.PauliString.Z {n : ℕ} (i : Fin n) : PauliString n

The single-site Z_i.

Equations

• Lean4LPD.PauliString.Z i = { x := 0, z := fun (j : Fin n) => if j = i then 1 else 0, phase := 0 }

The witness

n = 8, k_h = 2, w* = 1, and a brickwork of two-qubit generators.

def Lean4LPD.LayerWitness.L₁ : List (PauliString 8)

The even brickwork layer: generators on qubit pairs (0,1), (2,3), (4,5), (6,7).

Equations

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

def Lean4LPD.LayerWitness.L₂ : List (PauliString 8)

The odd brickwork layer: generators on (1,2), (3,4), (5,6).

Equations

• Lean4LPD.LayerWitness.L₂ = [Lean4LPD.PauliString.X 1 * Lean4LPD.PauliString.Z 2, Lean4LPD.PauliString.X 3 * Lean4LPD.PauliString.X 4, Lean4LPD.PauliString.X 5 * Lean4LPD.PauliString.X 6]

theorem Lean4LPD.LayerWitness.isLayer_L₁ : PauliString.IsLayer 2 L₁

Both layers are layers of 2-local generators with disjoint supports: k_h = 2.

theorem Lean4LPD.LayerWitness.isLayer_L₂ : PauliString.IsLayer 2 L₂

theorem Lean4LPD.LayerWitness.isSelfAdjoint_L₁ (G : PauliString 8) : G ∈ L₁ → IsSelfAdjoint G

Every generator used is a Hermitian Pauli string, so each layer really is a product of Pauli rotations e^{-iθG} with G† = G and G² = 1 (isSelfAdjoint_iff_mul_self_eq_one). None of them has a Y site, so phase 0 is the Hermitian representative.

theorem Lean4LPD.LayerWitness.isSelfAdjoint_L₂ (G : PauliString 8) : G ∈ L₂ → IsSelfAdjoint G

theorem Lean4LPD.LayerWitness.weight_Z_three : (PauliString.Z 3).weight = 1

The input is Z₃, a single-qubit Z, so its weight is 1. The input of a Trotter step has weight at most w* after the preceding truncation; here that means w* = 1.

theorem Lean4LPD.LayerWitness.isSelfAdjoint_Z_three : IsSelfAdjoint (PauliString.Z 3)

theorem Lean4LPD.LayerWitness.gamma_layers_weight_le (q : PauliString 8) : q ∈ PauliString.reachable [L₁, L₂] (PauliString.Z 3) → q.weight ≤ 4

After Γ layers the weight is at most w* k_h^Γ. With w* = 1, k_h = 2 and the Γ = 2 brickwork layers [L₁, L₂], nothing of weight more than w* k_h^Γ = 4 is reachable from Z₃. By gamma_layers_weight_four the value 4 is attained, so the bound k_h ^ L has no slack in its constant: the weight-6 string of gamma_weight_bound_false exceeds 4 only because a second-order step has more than Γ layers.

Nothing about the brickwork is used: this is reachable_weight_le at k_h = 2 and two layers.

The two named witnesses

Both are written with the phase #{Y-sites} mod 4 — the canonical signless representative in Pauli/Basic.lean's convention, which pins the sign that isSelfAdjoint_iff_phase alone leaves open. Hermiticity itself is checked below, so these are genuine observables, of the kind the discarded component Õ^{(d)}_{≥w*+1} of apd:eq:step_component is a combination of, and not phase-decorated artefacts of the branching.

def Lean4LPD.LayerWitness.P₄ : PauliString 8

The weight-4 witness: site types X Y Z X on qubits 1,2,3,4. Reachable from Z₃ in the Γ = 2 layers [L₁, L₂], where it attains the bound w* k_h^Γ = 4 exactly.

Equations

• Lean4LPD.LayerWitness.P₄ = { x := ![0, 1, 1, 0, 1, 0, 0, 0], z := ![0, 0, 1, 1, 0, 0, 0, 0], phase := 1 }

def Lean4LPD.LayerWitness.P₆ : PauliString 8

The weight-6 witness: site types X Y Y Z Y X on qubits 0,…,5. Reachable from Z₃ in [L₁, L₂, L₁]; its weight exceeds w* k_h^Γ = 4.

Equations

• Lean4LPD.LayerWitness.P₆ = { x := ![1, 1, 1, 0, 1, 1, 0, 0], z := ![0, 1, 1, 1, 1, 0, 0, 0], phase := 3 }

theorem Lean4LPD.LayerWitness.isSelfAdjoint_P₄ : IsSelfAdjoint P₄

theorem Lean4LPD.LayerWitness.isSelfAdjoint_P₆ : IsSelfAdjoint P₆

theorem Lean4LPD.LayerWitness.support_P₄ : P₄.support = {1, 2, 3, 4}

theorem Lean4LPD.LayerWitness.support_P₆ : P₆.support = {0, 1, 2, 3, 4, 5}

theorem Lean4LPD.LayerWitness.weight_P₄ : P₄.weight = 4

theorem Lean4LPD.LayerWitness.weight_P₆ : P₆.weight = 6

theorem Lean4LPD.LayerWitness.P₄_mem_reachable : P₄ ∈ PauliString.reachable [L₁, L₂] (PauliString.Z 3)

theorem Lean4LPD.LayerWitness.P₆_mem_reachable : P₆ ∈ PauliString.reachable [L₁, L₂, L₁] (PauliString.Z 3)

theorem Lean4LPD.LayerWitness.P₆_mem_reachable_unmerged : P₆ ∈ PauliString.reachable [L₁, L₂, L₂, L₁] (PauliString.Z 3)

The literal 2Γ = 4 layer reading, obtained from the merged one by letting P₆ sit out the repeated L₂: deciding this directly would re-explore the whole four-layer branching tree.

theorem Lean4LPD.LayerWitness.gamma_layers_weight_four : ∃ q ∈ PauliString.reachable [L₁, L₂] (PauliString.Z 3), q.weight = 4

…and the bound is attained: P₄ has weight exactly 4 and is reachable in the two brickwork layers. Together with gamma_layers_weight_le, the maximum reachable weight after Γ layers is exactly w* k_h^Γ.

theorem Lean4LPD.LayerWitness.gamma_weight_bound_false : ∃ q ∈ PauliString.reachable [L₁, L₂, L₁] (PauliString.Z 3), 4 < q.weight

A reachable string of weight 6 > w* k_h^Γ = 4 in a second-order step: the exponent of the light-cone bound has to count layers, not the Γ groups of the Hamiltonian.

With n = 8, k_h = 2, the two brickwork layers L₁, L₂ (so Γ = 2) and w* = 1, the value of w* k_h^Γ is 4. It is exactly the largest reachable weight after Γ layers (gamma_layers_weight_le and gamma_layers_weight_four), and it is exceeded after the layer sequence of the second-order product formula of apd:eq:suzuki, where the reachable Pauli P₆, supported on qubits 0,…,5 (support_P₆), has weight 6. This is consistent with reachable_weight_le, which allows weight up to k_h^3 = 8 for the three layers used here.

The layer sequence used here is [L₁, L₂, L₁], which is the second-order step L₁ L₂ · L₂ L₁ after the two adjacent H_Γ half-steps are merged: the shortest reading of a second-order step, and already one layer more than Γ. gamma_weight_bound_false_unmerged repeats it for the literal 2Γ = 4 layers.

This theorem is purely combinatorial: it contains no angle and no coefficient, and it does not quantify over the product-formula order p. That P₆ has a nonzero coefficient in the operator discarded after the second-order step is LayerCounterexample.actual_discard_exceeds_gamma_bound in Pauli/LayerCounterexample.lean.

theorem Lean4LPD.LayerWitness.gamma_weight_bound_false_unmerged : ∃ q ∈ PauliString.reachable [L₁, L₂, L₂, L₁] (PauliString.Z 3), 4 < q.weight

The same combinatorial witness for the literal 2Γ = 4 layers [L₁, L₂, L₂, L₁] of the second-order product formula (apd:eq:suzuki), with no merging of the two adjacent H_Γ half-steps.