The Pauli-layer inhabitant of the multi-jump ladder

This file instantiates the abstract MultiLadder of Ladder/MultiJump.lean with Pauli dynamics, which formalizes the recurrence of apd:rmk:multijump. A trajectory layerTraj alternates conjugation by a disjoint-support layer of Pauli rotations with truncation to an arbitrary retained set of Paulis, and layerN records its high-weight norms above the rungs w_m = k_o + (m - 1) (k_h - 1). The layer-inflow bound apd:thm:layer_inflow of LayerFlow.lean yields the multi-jump recurrence with the jump factors ε_j^{(m)} = (w_{m+j} a)^j / j! (epsJump) and the entry factor E_m = ∑_{j ≥ m} ε_j^{(m)} (entryFactor), where a bounds the absolute sines of all rotation angles. The abstract first-passage majorant apd:eq:composition_majorant then applies.

Main definitions

• layerTraj Ls S O: the trajectory O_{T+1} = truncOp (S T) (layerConj (Ls T) O_T), O_0 = O.
• layerN: the rung masses of layerTraj: the Pauli norm at rung 0 (the reservoir) and the high-weight norm above rungWeight ko kh m at rung m ≥ 1.
• pauliMultiLadder: the resulting MultiLadder (epsJump ..) (entryFactor ..) (pauliNorm O).

Main results

• summable_epsJump_tail, sum_Ico_epsJump_le_entryFactor: for β < 1 the entry series converges and dominates each of its finite partial sums.
• highNorm_layerConj_le_multi: the multi-jump inflow inequality of one layer, for an arbitrary operator.
• layerN_step: the recurrence of apd:rmk:multijump along layerTraj.
• layerN_le_majorant: the first-passage majorant apd:eq:composition_majorant for layerTraj.

Implementation notes

The hypotheses of pauliMultiLadder are: every layer has pairwise disjoint supports and Hermitian generators of weight at most k_h, with 2 ≤ k_h; |sin θ| ≤ a for every angle; betaOf < 1, which makes the entry series converge by comparison with a geometric series; and the input observable is k_o-local. The fields nonneg, init and step of MultiLadder are then theorems about layerTraj. The retained sets S T are arbitrary, so the construction covers truncation after every layer as well as truncation only at step boundaries (S T = univ in between).

layerN measures the operator that is kept along the trajectory. The operator discarded at a step boundary, Õ^{(d)}_{≥w*+1} of apd:eq:step_component, is a different object: its norm is a high-weight norm before the cut. The two are related in LayerError.lean.

theorem Lean4LPD.summable_epsJump_tail {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) {m : ℕ} (hm : 1 ≤ m) (hb : betaOf kh1 c a < 1) : Summable fun (i : ℕ) => epsJump kh1 c a (m + i) m

The entry series ∑_i ε_{m+i}^{(m)} of apd:eq:composition_majorant converges when β < 1: by epsJump_ratio each term is at most β times the previous one, so the series is dominated by a geometric series.

theorem Lean4LPD.sum_Ico_epsJump_le_entryFactor {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) {m : ℕ} (hm : 1 ≤ m) (hb : betaOf kh1 c a < 1) (K : ℕ) : ∑ j ∈ Finset.Ico m K, epsJump kh1 c a j m ≤ entryFactor kh1 c a m

Every finite partial sum ∑_{m ≤ j < K} ε_j^{(m)} is at most the entry factor E_m of apd:eq:composition_majorant, which is defined as the infinite sum.

theorem Lean4LPD.epsJump_nonneg_all {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (j m : ℕ) : 0 ≤ epsJump kh1 c a j m

The jump factors ε_j^{(m)} of apd:rmk:multijump are nonnegative for all indices. The ladder recurrence only sums over j ≥ 1; the case j = 0, where the formula gives ε_0^{(m)} = 1, is included because MultiLadder.le_majorant asks for nonnegativity at all indices.

theorem Lean4LPD.entryFactor_nonneg_all {kh1 c a : ℝ} (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (m : ℕ) : 0 ≤ entryFactor kh1 c a m

The entry factors E_m of apd:eq:composition_majorant are nonnegative.

theorem Lean4LPD.PauliString.rungWeight_cast_eq_rungW {ko kh m : ℕ} (hkh : 2 ≤ kh) (hm : 1 ≤ m) : ↑(rungWeight ko kh m) = rungW (↑(kh - 1)) (↑ko / ↑(kh - 1)) m

The natural-number rung threshold rungWeight ko kh m = k_o + (m - 1) (k_h - 1) equals the real-valued rung rungW (k_h - 1) (k_o / (k_h - 1)) m that enters epsJump (apd:rmk:multijump). Under 2 ≤ k_h and 1 ≤ m the natural subtractions k_h - 1 and m - 1 are exact, so they agree with the real ones.

theorem Lean4LPD.PauliString.rungWeight_add_jump (ko kh m j : ℕ) (hm : 1 ≤ m) : rungWeight ko kh m + j * (kh - 1) = rungWeight ko kh (m + j)

Adding j rung spacings k_h - 1 to rung m ≥ 1 gives rung m + j, the index that appears in the coefficient ε_j^{(m)} of apd:rmk:multijump.

theorem Lean4LPD.PauliString.rungWeight_sub_jump (ko kh m j : ℕ) (hj : j < m) : rungWeight ko kh (m - j) + j * (kh - 1) = rungWeight ko kh m

A j-jump with j < m enters rung m from the positive rung m - j (apd:rmk:multijump). Since j < m, the natural subtraction m - j is exact.

theorem Lean4LPD.PauliString.layer_factor_eq_epsJump {ko kh m : ℕ} (hkh : 2 ≤ kh) (hm : 1 ≤ m) (a : ℝ) (j : ℕ) : (↑(rungWeight ko kh m + j * (kh - 1)) * a) ^ j / ↑j.factorial = epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a j m

The factorial coefficient of the layer-inflow bound norm_layerInflowMatrix_le_factorial at the threshold w_m is exactly the jump factor ε_j^{(m)} (apd:eq:layer_inflow; apd:rmk:multijump).

noncomputable def Lean4LPD.PauliString.layerTraj {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) : ℕ → Matrix (Bits n) (Bits n) ℂ

The truncated layer trajectory of apd:rmk:multijump: at time T, conjugate by the layer Ls T and then project onto the retained set S T. The trajectory is defined at operator level; its rung masses layerN are computed from it, and their recurrence is a theorem (layerN_step).

Equations

• Lean4LPD.PauliString.layerTraj Ls S O 0 = O
• Lean4LPD.PauliString.layerTraj Ls S O T.succ = Lean4LPD.PauliString.truncOp (S T) (Lean4LPD.PauliString.layerConj (Ls T) (Lean4LPD.PauliString.layerTraj Ls S O T))

@[simp]

theorem Lean4LPD.PauliString.layerTraj_zero {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) : layerTraj Ls S O 0 = O

The trajectory of apd:rmk:multijump starts at the input observable itself: no truncation is applied at time 0.

theorem Lean4LPD.PauliString.layerTraj_succ {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) (T : ℕ) : layerTraj Ls S O (T + 1) = truncOp (S T) (layerConj (Ls T) (layerTraj Ls S O T))

One step of the trajectory of apd:rmk:multijump: evolve through a layer, then cut.

theorem Lean4LPD.PauliString.pauliNorm_layerConj {n : ℕ} (L : List (PauliString n × ℝ)) (hL : ∀ g ∈ L, IsSelfAdjoint g.1) (O : Matrix (Bits n) (Bits n) ℂ) : pauliNorm (layerConj L O) = pauliNorm O

Conjugation by a whole layer of Hermitian generators preserves the Pauli norm, by the coefficient isometry norm_layerAct. This is one half of the reservoir bound in apd:rmk:multijump.

theorem Lean4LPD.PauliString.pauliNorm_layerTraj_le {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (hL : ∀ (T : ℕ), ∀ g ∈ Ls T, IsSelfAdjoint g.1) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) (T : ℕ) : pauliNorm (layerTraj Ls S O T) ≤ pauliNorm O

The Pauli norm along the truncated trajectory never exceeds that of the input, since layers preserve it and truncation cannot increase it. This is the reservoir bound of apd:rmk:multijump.

noncomputable def Lean4LPD.PauliString.layerN {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) (ko kh : ℕ) : ℕ → ℕ → ℝ

The rung masses of the truncated trajectory: the total Pauli norm at rung 0, and the high-weight norm above rungWeight ko kh m at rung m ≥ 1. This is the field N of the MultiLadder for apd:rmk:multijump.

Equations

• Lean4LPD.PauliString.layerN Ls S O ko kh 0 x✝ = Lean4LPD.PauliString.pauliNorm (Lean4LPD.PauliString.layerTraj Ls S O x✝)
• Lean4LPD.PauliString.layerN Ls S O ko kh m.succ x✝ = Lean4LPD.PauliString.highNorm (Lean4LPD.rungWeight ko kh (m + 1)) (Lean4LPD.PauliString.layerTraj Ls S O x✝)

theorem Lean4LPD.PauliString.layerN_eq_highNorm {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) (ko kh m T : ℕ) (hm : 1 ≤ m) : layerN Ls S O ko kh m T = highNorm (rungWeight ko kh m) (layerTraj Ls S O T)

At every positive rung, layerN is the high-weight norm of the truncated trajectory (apd:rmk:multijump).

theorem Lean4LPD.PauliString.layerN_nonneg {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) (ko kh m T : ℕ) : 0 ≤ layerN Ls S O ko kh m T

The rung masses of the truncated trajectory are nonnegative (apd:rmk:multijump).

theorem Lean4LPD.PauliString.layerN_init {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) {O : Matrix (Bits n) (Bits n) ℂ} {ko kh : ℕ} (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (m : ℕ) (hm : 1 ≤ m) : layerN Ls S O ko kh m 0 = 0

A k_o-local input observable has no mass above any positive rung, since k_o ≤ rungWeight ko kh m. This is the initial condition in apd:rmk:multijump.

theorem Lean4LPD.PauliString.highNorm_layerConj_le_multi {n : ℕ} (L : List (PauliString n × ℝ)) {ko kh m : ℕ} (hkh : 2 ≤ kh) (hL : IsLayer kh (List.map Prod.fst L)) (hherm : ∀ g ∈ L, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ g ∈ L, |Real.sin g.2| ≤ a) (hm : 1 ≤ m) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (O : Matrix (Bits n) (Bits n) ℂ) : highNorm (rungWeight ko kh m) (layerConj L O) ≤ highNorm (rungWeight ko kh m) O + ∑ j ∈ Finset.Ico 1 m, epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a j m * highNorm (rungWeight ko kh (m - j)) O + entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a m * pauliNorm O

Multi-jump flow through one layer. For an arbitrary operator O, the high-weight norm above rung m after a disjoint-support layer is at most its value before the layer, plus the j-jump inflows ε_j^{(m)} from the positive rungs m - j, plus the entry factor E_m times the Pauli norm of O. This derives the recurrence of apd:rmk:multijump from apd:thm:layer_inflow: jumps with j < m are localized on rung m - j, and the finitely many jumps with j ≥ m are bounded by the full norm and then by the infinite sum E_m.

theorem Lean4LPD.PauliString.layerN_step {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh : ℕ} (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (Ls T))) (hherm : ∀ (T : ℕ), ∀ g ∈ Ls T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ Ls T, |Real.sin g.2| ≤ a) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (m T : ℕ) (hm : 1 ≤ m) : layerN Ls S O ko kh m (T + 1) ≤ layerN Ls S O ko kh m T + ∑ j ∈ Finset.Ico 1 m, epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a j m * layerN Ls S O ko kh (m - j) T + entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a m * pauliNorm O

The multi-jump recurrence along the truncated layer trajectory. This is the step field of MultiLadder for apd:rmk:multijump, with the factorial jump factors epsJump and the infinite-sum entry factor entryFactor. It combines highNorm_layerConj_le_multi with the facts that truncation does not increase high-weight norms and that the Pauli norm along the trajectory is at most that of the input.

noncomputable def Lean4LPD.PauliString.pauliMultiLadder {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh : ℕ} (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (Ls T))) (hherm : ∀ (T : ℕ), ∀ g ∈ Ls T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ Ls T, |Real.sin g.2| ≤ a) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) : MultiLadder (epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (pauliNorm O)

The Pauli-layer MultiLadder, with the jump factors epsJump and the entry factors entryFactor of apd:rmk:multijump. It formalizes the recurrence underlying apd:eq:composition_majorant. The fields nonneg, init and step are theorems about layerTraj; the hypotheses are only the layer structure, Hermiticity of the generators, the sine bound, betaOf < 1 and k_o-locality of O. The ladder controls the rung masses of the kept operator; the discarded operator Õ^{(d)}_{≥w*+1} is treated in LayerError.lean.

Equations

• Lean4LPD.PauliString.pauliMultiLadder Ls S O hkh hL hherm ha hsin hb hloc = { N := Lean4LPD.PauliString.layerN Ls S O ko kh, nonneg := ⋯, init := ⋯, step := ⋯ }

theorem Lean4LPD.PauliString.layerN_le_majorant {n : ℕ} (Ls : ℕ → List (PauliString n × ℝ)) (S : ℕ → Finset (PauliIndex n)) (O : Matrix (Bits n) (Bits n) ℂ) {ko kh : ℕ} (hkh : 2 ≤ kh) (hL : ∀ (T : ℕ), IsLayer kh (List.map Prod.fst (Ls T))) (hherm : ∀ (T : ℕ), ∀ g ∈ Ls T, IsSelfAdjoint g.1) {a : ℝ} (ha : 0 ≤ a) (hsin : ∀ (T : ℕ), ∀ g ∈ Ls T, |Real.sin g.2| ≤ a) (hb : betaOf (↑(kh - 1)) (↑ko / ↑(kh - 1)) a < 1) (hloc : ∀ (p : PauliIndex n), ko < wt p → coeff O p = 0) (T m : ℕ) (hm : 1 ≤ m) : layerN Ls S O ko kh m T ≤ MultiLadder.majorant (epsJump (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (entryFactor (↑(kh - 1)) (↑ko / ↑(kh - 1)) a) (pauliNorm O) m T

The first-passage majorant for truncated Pauli layers. The abstract bound MultiLadder.le_majorant (apd:eq:composition_majorant) applied to pauliMultiLadder: the mass of layerTraj above every rung m ≥ 1 is at most the majorant built from epsJump and entryFactor.