The damped local norm flow, and the Pauli inhabitant of Ladder

This file proves apd:thm:local_flow_k_local, the damped local norm flow on which the quantitative truncation-error analysis of LPD rests:

N_{≥m}^{(g)} ≤ N_{≥m}^{(g-1)} + sin(dt)·N_{≥m-1}^{(g-1)}.

Here N_{≥m}^{(g)} is the high-weight norm (apd:eq:def_high_weight_norm) of the observable after g Pauli rotations, taken above the rung weight w_m = k_o + (m-1)(k_h-1). The file then uses the inequality to construct an instance of the abstract structure Lean4LPD.Ladder, whose step field is exactly this recursion. The consequences of the recursion are proved in Ladder/ for an abstract ladder, with no Pauli infrastructure, so the instance is what makes them apply to the Pauli model.

Main definitions

• PauliString.partner, PauliString.partnerSign: the pairing s ↔ ±i G s of the classes that anticommute with G, and the sign relating i G s to the self-adjoint representative herm.
• PauliString.rotAct: the action of conjugation by one Pauli rotation on coefficient vectors.
• PauliString.traj: the Heisenberg trajectory O^{(g)} = U_g† O U_g.
• PauliString.ladderN: the family N m g of high-weight norms along the trajectory.
• PauliString.pauliLadder, PauliString.pauliWeightedLadder, PauliString.pauliLadderOfHerm: the instances of Ladder and WeightedLadder.

Main results

• PauliString.coeffVec_conj: conjugation by one rotation acts on coefficient vectors as rotAct.
• PauliString.norm_rotAct: rotAct is an isometry of ℓ².
• PauliString.norm_restr_high_rotAct_low: the inflow into the high-weight region is at most |sin θ| times the mass on the partners.
• PauliString.highNorm_conj_le_highNorm, PauliString.local_flow_k_local: apd:thm:local_flow_k_local for one rotation, at general thresholds and at the rung weights.
• PauliString.highNorm_conj_le_pauliNorm: the form used at rung 1, with the total mass on the right.
• PauliString.pauliNorm_conj, PauliString.pauliNorm_traj: unitary invariance of the Pauli 2-norm.
• PauliString.highNorm_restr_le: restriction (truncation) only decreases high-weight norms.

The one-rotation theorems assume only that the generator is a Hermitian Pauli string of weight at most k_h; they hold for every operator O and every angle. In particular no locality hypothesis on the observable is needed, which is stronger than the paper's statement. Locality of the initial observable enters only through the init field of pauliLadder.

The argument

The proof follows the paper's, in four moves.

1. The coefficient vector — Pauli/Coeff.lean, with ‖O‖_{2,normalized} = ‖x‖_{ℓ²}.
2. Conjugation acts as a real orthogonal matrix A: commuting classes are fixed, anticommuting ones pair up as s ↔ ±i G s, and A is a planar rotation on each pair. Here that is rotAct, and it is a theorem about the coefficients (coeffVec_conj) rather than a description: Pauli/Branch.lean's pauli_rotation_branch_anticommute_hermitian supplies the operator identity (apd:eq:pauli_rotation_branch), trace cyclicity moves the conjugation onto the Pauli, and partnerSign is the sign of ±i G s, which becomes part of the matrix entry. Orthogonality is norm_rotAct.
3. ‖A_RR‖ ≤ 1: a submatrix of an orthogonal matrix has operator norm at most one. BlockNorm.lean proves exactly that statement, but it is not what is used here: no matrix A is ever built, so the corresponding step is ‖restr R (rotAct G θ v)‖ ≤ ‖rotAct G θ v‖ = ‖v‖, i.e. norm_restr_le composed with the isometry. Same content, one fewer object.
4. The inflow ‖A_RB x_B‖ ≤ sin(dt)·N_{≥m-1} — norm_restr_high_rotAct_low. The weight step is weight_le_weight_mul_add_kh, whose k_h − 1 (rather than k_h) holds only because the pairing is between anticommuting Paulis; see Pauli/Weight.lean.

Minkowski's inequality is norm_add_le on EuclideanSpace.

What is proved, and what is assumed

local_flow_k_local is the inequality for one rotation at rung m ≥ 2, in the variables w_m = k_o + (m-1)(k_h-1). pauliLadder is the Ladder instance, hence the inequality along a whole trajectory, at every rung, and pauliWeightedLadder is the same family as a WeightedLadder. MultiLadder is not inhabited here: its step is the multi-jump recursion of apd:thm:layer_inflow, about a layer of disjointly supported rotations; that instance is pauliMultiLadder in Pauli/LayerLadder.lean.

Three things to read narrowly.

• a is |sin(dt)|, not sin(dt). pauliLadder takes any a dominating every |sin(θ_g)|, which is what the estimate gives with no sign hypothesis on the angles.
• Rung 0 is the reservoir, not rungWeight ko kh 0. Ladder/Defs.lean explains why: truncated ℕ subtraction makes rungWeight ko kh 0 = k_o, whereas the model wants w_0 = k_o - (k_h-1). So ladderN sets N 0 g := ‖O^{(g)}‖_{2,normalized}, which satisfies reservoir with equality by unitary invariance (pauliNorm_traj; this is the base case of apd:cor:norm_cumulation_jump). step at m = 1 is then highNorm_conj_le_pauliNorm, which bounds the inflow by the total mass. Since the total mass dominates every high-weight norm (highNorm_le_pauliNorm), this reading makes step at m = 1 weaker than the flow bound with a genuine weight threshold w_0 on the right, and unlike that bound it needs no condition relating k_o and k_h.
• The trajectory here carries no truncation. Truncation zeroes coefficients and so only decreases every N_{≥m}, which is why apd:cor:norm_cumulation_jump holds along the truncated LPD trajectory as well. highNorm_restr_le is that statement on the coefficient side, but traj itself is the untruncated U_g† O U_g; the truncated trajectory and its ladder are in Pauli/Truncate.lean.

The flow is stated with the closed-form rotation rot and the entrywise Pauli matrices toMatrix. That rot is the matrix exponential and that toMatrix is the correctly phased tensor product are proved separately, in RotationExp.lean and Pauli/Tensor.lean.

The coefficient vector in the paper's proof is real. That is not formalized as a property of the scalars: coeff O p : ℂ. It is not needed — the transformation is by real planar rotations, and ∑ |x_p|² is preserved for the same reason ∑ x_p² would be. What is used is that the partner i G s is a Hermitian Pauli (isSelfAdjoint_phaseMul_one_mul), which is what makes the coefficient sin θ on it real.

The partner pairing on classes

In the proof of apd:thm:local_flow_k_local the Paulis that anticommute with the generator G are grouped into unordered pairs {s, s'}, where s' = ±i G s is the partner of s, determined up to sign. On classes that pairing is the translation p ↦ (G.x + p.x, G.z + p.z), and it is an involution because the X- and Z-parts live in characteristic two.

def Lean4LPD.PauliString.partner {n : ℕ} (G : PauliString n) (p : PauliIndex n) : PauliIndex n

The partner class of p under G: the class of G · herm p, hence of the partner ±i G s of s = herm p.

Equations

• G.partner p = (G.x + p.1, G.z + p.2)

@[simp]

theorem Lean4LPD.PauliString.cls_mul_herm {n : ℕ} (G : PauliString n) (p : PauliIndex n) : (G * herm p).cls = G.partner p

@[simp]

theorem Lean4LPD.PauliString.partner_partner {n : ℕ} (G : PauliString n) (p : PauliIndex n) : G.partner (G.partner p) = p

The pairing is an involution, which is what lets {s, s'} be an unordered pair at all. That it has no fixed point on the anticommuting sector is also true — a fixed point would make G a phase, which commutes with everything — but it is not proved here and not needed: Finset.sum_involution discharges a fixed point on its own, since f p + f p = 0 forces f p = 0.

theorem Lean4LPD.PauliString.partner_injective {n : ℕ} (G : PauliString n) : Function.Injective G.partner

@[simp]

theorem Lean4LPD.PauliString.sympForm_herm_partner {n : ℕ} (G : PauliString n) (p : PauliIndex n) : G.sympForm (herm (G.partner p)) = G.sympForm (herm p)

The partner still anticommutes with the generator, stated on classes: G has the same symplectic form with the partner of p as with p. This is what makes the pairing preserve the anticommuting sector.

theorem Lean4LPD.PauliString.wt_partner {n : ℕ} (G : PauliString n) (p : PauliIndex n) : wt (G.partner p) = (G * herm p).weight

The partner class has the weight of the product G · herm p, which is what Pauli/Weight.lean's bounds are about.

The sign absorbed into the matrix entry

The partner of s is i G s only up to a sign, which depends on the representative chosen in the partner's class; that sign becomes part of the matrix entry of the planar rotation. partnerSign is that sign, and partnerSign_partner is the antisymmetry that makes the planar rotation on the pair {s, s'} an orthogonal map rather than merely a bounded one.

noncomputable def Lean4LPD.PauliString.partnerSign {n : ℕ} (G : PauliString n) (p : PauliIndex n) : ℂ

The sign relating the Hermitian partner i G s to the canonical self-adjoint representative of its class: toMatrix (i G herm p) = partnerSign G p • toMatrix (herm (partner G p)).

Equations

• G.partnerSign p = Lean4LPD.iPow ((Lean4LPD.PauliString.phaseMul 1 (G * Lean4LPD.PauliString.herm p)).phase - (Lean4LPD.PauliString.herm (G.partner p)).phase)

theorem Lean4LPD.PauliString.toMatrix_partner {n : ℕ} (G : PauliString n) (p : PauliIndex n) : (phaseMul 1 (G * herm p)).toMatrix = G.partnerSign p • (herm (G.partner p)).toMatrix

The defining property of partnerSign.

theorem Lean4LPD.PauliString.partnerSign_eq_one_or_neg_one {n : ℕ} {G : PauliString n} {p : PauliIndex n} (hG : IsSelfAdjoint G) (h : G.sympForm (herm p) = 1) : G.partnerSign p = 1 ∨ G.partnerSign p = -1

partnerSign is a sign: the two self-adjoint representatives of a class differ by ±1 (phase_sub_of_isSelfAdjoint), and i G s is self-adjoint when G and s are self-adjoint and anticommute (isSelfAdjoint_phaseMul_one_mul).

theorem Lean4LPD.PauliString.partnerSign_mul_self {n : ℕ} {G : PauliString n} {p : PauliIndex n} (hG : IsSelfAdjoint G) (h : G.sympForm (herm p) = 1) : G.partnerSign p * G.partnerSign p = 1

theorem Lean4LPD.PauliString.norm_partnerSign {n : ℕ} {G : PauliString n} {p : PauliIndex n} (hG : IsSelfAdjoint G) (h : G.sympForm (herm p) = 1) : ‖G.partnerSign p‖ = 1

theorem Lean4LPD.PauliString.conj_partnerSign {n : ℕ} {G : PauliString n} {p : PauliIndex n} (hG : IsSelfAdjoint G) (h : G.sympForm (herm p) = 1) : (starRingEnd ℂ) (G.partnerSign p) = G.partnerSign p

theorem Lean4LPD.PauliString.partnerSign_partner {n : ℕ} {G : PauliString n} {p : PauliIndex n} (hG : IsSelfAdjoint G) (h : G.sympForm (herm p) = 1) : G.partnerSign (G.partner p) = -G.partnerSign p

The signs on a pair are opposite. The map s ↦ i G s squares to -1, not to the identity: i G (i G s) = -s. Consequently the two entries of the planar rotation on {s, s'} carry opposite signs, which is exactly what makes it a rotation.

Conjugation as an orthogonal map A on coefficient vectors

noncomputable def Lean4LPD.PauliString.rotAct {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : EuclideanSpace ℂ (PauliIndex n)

The orthogonal matrix A of the proof of apd:thm:local_flow_k_local, as a map on coefficient vectors (no matrix is built): the identity on classes commuting with G, and the planar rotation x_s ↦ cos(θ)x_s ∓ sin(θ)x_{s'} on each anticommuting pair, with the sign given by partnerSign. That this is conjugation is coeffVec_conj; that it is orthogonal is norm_rotAct.

Equations

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

@[simp]

theorem Lean4LPD.PauliString.rotAct_apply {n : ℕ} (G : PauliString n) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (p : PauliIndex n) : (G.rotAct θ y).ofLp p = if G.sympForm (herm p) = 0 then y.ofLp p else ↑(Real.cos θ) * y.ofLp p - ↑(Real.sin θ) * (G.partnerSign p * y.ofLp (G.partner p))

theorem Lean4LPD.PauliString.rotAct_add {n : ℕ} (G : PauliString n) (θ : ℝ) (y z : EuclideanSpace ℂ (PauliIndex n)) : G.rotAct θ (y + z) = G.rotAct θ y + G.rotAct θ z

theorem Lean4LPD.PauliString.coeff_conj {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (p : PauliIndex n) : coeff (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) p = if G.sympForm (herm p) = 0 then coeff O p else ↑(Real.cos θ) * coeff O p - ↑(Real.sin θ) * (G.partnerSign p * coeff O (G.partner p))

Conjugation by one rotation acts on the coefficient vector as A, coefficient by coefficient.

Trace cyclicity moves the conjugation from O onto the Pauli, where pauli_rotation_branch_anticommute_hermitian (apd:eq:pauli_rotation_branch, in its Hermitian-partner form) applies at angle -θ.

theorem Lean4LPD.PauliString.coeffVec_conj {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : coeffVec (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) = G.rotAct θ (coeffVec O)

coeff_conj as a statement about the vector.

A is orthogonal

The pairs {s, s'} partition the anticommuting sector, so the sum of |x_p|² splits into the fixed classes and the pairs, and on each pair the cross term cancels because partnerSign is antisymmetric.

theorem Lean4LPD.PauliString.norm_rotAct {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖G.rotAct θ y‖ = ‖y‖

Conjugation is orthogonal on coefficient vectors: rotAct G θ preserves the ℓ² norm, for every Hermitian Pauli string G and every angle θ.

The inflow bound

theorem Lean4LPD.PauliString.norm_restr_high_rotAct_low {n : ℕ} {G : PauliString n} {w : ℕ} (hG : IsSelfAdjoint G) (θ : ℝ) (y : EuclideanSpace ℂ (PauliIndex n)) (T : Finset (PauliIndex n)) (hT : ∀ (q : PauliIndex n), w < wt q → G.sympForm (herm q) = 1 → G.partner q ∈ T) : ‖restr (highSet n w) (G.rotAct θ (restr (highSet n w)ᶜ y))‖ ≤ |Real.sin θ| * ‖restr T y‖

The inflow into the high-weight region. The only classes A maps into R from outside it are partners of high-weight anticommuting classes, each with entry ±sin(θ); T is any set of classes containing those partners.

The damped local norm flow

theorem Lean4LPD.PauliString.highNorm_conj_le {n : ℕ} {G : PauliString n} {w : ℕ} (hG : IsSelfAdjoint G) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (T : Finset (PauliIndex n)) (hT : ∀ (q : PauliIndex n), w < wt q → G.sympForm (herm q) = 1 → G.partner q ∈ T) : highNorm w (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) ≤ highNorm w O + |Real.sin θ| * ‖restr T (coeffVec O)‖

One rotation, with a general target set. The high-weight norm above w grows by at most |sin θ| times the ℓ² mass on any set T of classes that contains the partner of every anticommuting class of weight above w. This is the shape of apd:thm:local_flow_k_local; the choice of T is where the weight bound |i G s| ≥ |s| - (k_h-1) on the partner enters, in highNorm_conj_le_highNorm.

theorem Lean4LPD.PauliString.highNorm_conj_le_highNorm {n : ℕ} {G : PauliString n} {kh w w' : ℕ} (hG : IsSelfAdjoint G) (hk : G.weight ≤ kh) (hw : w' + (kh - 1) ≤ w) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : highNorm w (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) ≤ highNorm w O + |Real.sin θ| * highNorm w' O

apd:thm:local_flow_k_local for one rotation, at a pair of thresholds w' + (k_h - 1) ≤ w. Consecutive rung weights satisfy this with equality, w_m - (k_h-1) = w_{m-1} (rungWeight_add_two).

theorem Lean4LPD.PauliString.highNorm_conj_le_pauliNorm {n : ℕ} {G : PauliString n} {w : ℕ} (hG : IsSelfAdjoint G) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : highNorm w (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) ≤ highNorm w O + |Real.sin θ| * pauliNorm O

The same bound with the total mass on the right — the form the ladder needs at rung 1, where w_0 is the reservoir rather than a weight (see Ladder/Defs.lean).

theorem Lean4LPD.PauliString.pauliNorm_conj {n : ℕ} {G : PauliString n} (hG : IsSelfAdjoint G) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : pauliNorm (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) = pauliNorm O

Unitary invariance of the Pauli 2-norm under conjugation by one rotation, which is what the ladder's reservoir field rests on (the base case of apd:cor:norm_cumulation_jump). Proved from Parseval and orthogonality of A, not from a separate Hilbert–Schmidt argument.

theorem Lean4LPD.PauliString.highNorm_restr_le {n w : ℕ} (S : Finset (PauliIndex n)) (y : EuclideanSpace ℂ (PauliIndex n)) : ‖restr (highSet n w) (restr S y)‖ ≤ ‖restr (highSet n w) y‖

Truncation only decreases the high-weight norms: restricting a coefficient vector to any set of classes cannot increase its mass above any threshold.

theorem Lean4LPD.PauliString.rungWeight_add_two (ko kh m : ℕ) : rungWeight ko kh (m + 2) = rungWeight ko kh (m + 1) + (kh - 1)

The rung spacing is exactly k_h − 1, which is what makes highNorm_conj_le_highNorm's hypothesis an equality at consecutive rungs. Stated from rung 1 upwards, where rungWeight's truncated subtraction is the intended value.

The trajectory, and the Ladder instance

noncomputable def Lean4LPD.PauliString.traj {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

The evolved observable O^{(g)} = U_g† O U_g of apd:thm:local_flow_k_local, where U_g is the product of the first g rotations e^{-i G_l θ_l/2}. In Rotation.lean's angle convention rot G θ is the + exponential e^{+i G θ/2}, so one step of the Heisenberg evolution is O ↦ rot G θ * O * rot G (-θ) and the conjugation angle is θ.

Equations

• Lean4LPD.PauliString.traj Gs θ O 0 = O
• Lean4LPD.PauliString.traj Gs θ O g.succ = Lean4LPD.rot (Gs g).toMatrix (θ g) * Lean4LPD.PauliString.traj Gs θ O g * Lean4LPD.rot (Gs g).toMatrix (-θ g)

@[simp]

theorem Lean4LPD.PauliString.traj_zero {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : traj Gs θ O 0 = O

theorem Lean4LPD.PauliString.traj_succ {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (g : ℕ) : traj Gs θ O (g + 1) = rot (Gs g).toMatrix (θ g) * traj Gs θ O g * rot (Gs g).toMatrix (-θ g)

theorem Lean4LPD.PauliString.pauliNorm_traj {n : ℕ} {Gs : ℕ → PauliString n} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (g : ℕ) : pauliNorm (traj Gs θ O g) = pauliNorm O

The total mass is conserved along the trajectory: ‖O^{(g)}‖_{2,normalized} = ‖O‖_{2,normalized} for every g.

noncomputable def Lean4LPD.PauliString.ladderN {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (ko kh : ℕ) : ℕ → ℕ → ℝ

The ladder family N m g := ‖(U_g† O U_g)_{≥ w_m + 1}‖_{2,normalized} (apd:eq:def_high_weight_norm), with rung 0 the reservoir ‖O^{(g)}‖_{2,normalized}.

Equations

• Lean4LPD.PauliString.ladderN Gs θ O ko kh 0 x✝ = Lean4LPD.PauliString.pauliNorm (Lean4LPD.PauliString.traj Gs θ O x✝)
• Lean4LPD.PauliString.ladderN Gs θ O ko kh m.succ x✝ = Lean4LPD.PauliString.highNorm (Lean4LPD.rungWeight ko kh (m + 1)) (Lean4LPD.PauliString.traj Gs θ O x✝)

theorem Lean4LPD.PauliString.ladderN_nonneg {n : ℕ} (Gs : ℕ → PauliString n) (θ : ℕ → ℝ) (O : Matrix (Bits n) (Bits n) ℂ) (ko kh m g : ℕ) : 0 ≤ ladderN Gs θ O ko kh m g

theorem Lean4LPD.PauliString.ladderN_init {n : ℕ} {Gs : ℕ → PauliString n} {θ : ℕ → ℝ} {O : Matrix (Bits n) (Bits n) ℂ} {ko kh : ℕ} (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (m : ℕ) (hm : 1 ≤ m) : ladderN Gs θ O ko kh m 0 = 0

The ladder's init: a k_o-local observable carries no mass above any rung m ≥ 1, since w_m ≥ w_1 = k_o.

noncomputable def Lean4LPD.PauliString.pauliLadder {n : ℕ} {Gs : ℕ → PauliString n} {θ : ℕ → ℝ} {O : Matrix (Bits n) (Bits n) ℂ} {ko kh : ℕ} {a : ℝ} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (hk : ∀ (g : ℕ), (Gs g).weight ≤ kh) (ha : ∀ (g : ℕ), |Real.sin (θ g)| ≤ a) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : Ladder a (pauliNorm O)

The Pauli model inhabits Lean4LPD.Ladder, and step is a theorem.

apd:thm:local_flow_k_local discharges the step field, so every consequence proved for an abstract Ladder applies to the Pauli model.

The hypotheses are: each generator is a Hermitian Pauli of weight at most k_h, the initial observable is k_o-local, and a dominates every |sin(θ_g)|. Locality is read through the coefficient vector (cf. def:support): every class carrying a non-zero coefficient has weight at most k_o.

Equations

• Lean4LPD.PauliString.pauliLadder hG hk ha hloc = { N := Lean4LPD.PauliString.ladderN Gs θ O ko kh, nonneg := ⋯, reservoir := ⋯, init := ⋯, step := ⋯ }

noncomputable def Lean4LPD.PauliString.pauliWeightedLadder {n : ℕ} {Gs : ℕ → PauliString n} {θ : ℕ → ℝ} {O : Matrix (Bits n) (Bits n) ℂ} {ko kh : ℕ} {c : ℕ → ℝ} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (hk : ∀ (g : ℕ), (Gs g).weight ≤ kh) (hc : ∀ (g m : ℕ), |Real.sin (θ g)| ≤ c m) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : WeightedLadder c (pauliNorm O)

The same family inhabits Lean4LPD.WeightedLadder.

WeightedLadder's fields are Ladder's with the constant a of step replaced by a rung-dependent c m, so the Pauli model supplies it for any c dominating every |sin(θ_g)|. Note that the flow bound itself is not rung-dependent — apd:thm:local_flow_k_local carries the same sin(dt) at every rung — so a constant c is the natural instance here. The rung dependence Ladder/Weighted.lean exploits enters later, from the per-layer factors w_{j+1} sin(dt) of apd:cor:norm_cumulation_jump (which come from apd:thm:layer_inflow), not from this lemma. What this discharges is applicability: every theorem stated over WeightedLadder has a Pauli instance.

Equations

• Lean4LPD.PauliString.pauliWeightedLadder hG hk hc hloc = { N := Lean4LPD.PauliString.ladderN Gs θ O ko kh, nonneg := ⋯, reservoir := ⋯, init := ⋯, step := ⋯ }

noncomputable def Lean4LPD.PauliString.pauliLadderOfHerm {n : ℕ} {Gs : ℕ → PauliString n} {θ : ℕ → ℝ} {kh : ℕ} {a : ℝ} (hG : ∀ (g : ℕ), IsSelfAdjoint (Gs g)) (hk : ∀ (g : ℕ), (Gs g).weight ≤ kh) (ha : ∀ (g : ℕ), |Real.sin (θ g)| ≤ a) (q : PauliIndex n) : Ladder a (pauliNorm (herm q).toMatrix)

A single Pauli observable inhabits the ladder, so pauliLadder's hypotheses are not satisfiable only in principle. Locality is coeff_toMatrix_herm_eq_zero: a basis Pauli's coefficient vector is a unit vector, hence carries nothing above weight |q|.

Equations

• Lean4LPD.PauliString.pauliLadderOfHerm hG hk ha q = Lean4LPD.PauliString.pauliLadder hG hk ha ⋯

theorem Lean4LPD.PauliString.local_flow_k_local {n : ℕ} {G : PauliString n} {kh ko m : ℕ} (hG : IsSelfAdjoint G) (hk : G.weight ≤ kh) (hm : 2 ≤ m) (θ : ℝ) (O : Matrix (Bits n) (Bits n) ℂ) : highNorm (rungWeight ko kh m) (rot G.toMatrix θ * O * rot G.toMatrix (-θ)) ≤ highNorm (rungWeight ko kh m) O + |Real.sin θ| * highNorm (rungWeight ko kh (m - 1)) O

apd:thm:local_flow_k_local, in the paper's variables.

For a Hermitian k_h-local generator and a rung m ≥ 2, the high-weight norm above w_m = k_o + (m-1)(k_h-1) grows by at most |sin(dt)| times the norm above w_{m-1}. Rung 1 needs highNorm_conj_le_pauliNorm instead, which bounds the inflow by the total mass; rung 0 is the reservoir, not a weight.

The inequality holds for every operator O and every angle θ: no locality hypothesis on the observable is used, which is stronger than the paper's statement. Here k_o only fixes the rung weights.