Globally sampled mass of an abstract multi-jump ladder

This file bounds the sum ∑_{d=1}^{r} N m (dΓ) of the rung masses of an abstract MultiLadder, sampled at the end of each block of Γ layers, by summing the first-passage majorant over the blocks (MultiLadder.sum_steps_le).

sum_steps_le is a general bound on the abstract ladder. It does not identify the sampled quantity with the components discarded by the truncation: along a truncated trajectory the mass above the truncation rung is zero at every block boundary, where it has just been cut, even when the discarded component is nonzero (retained_mass_ne_discarded_norm in tests/AssemblyBound.lean).

The per-step summation of apd:eq:total_high_weight_norm is handled by Lean4LPD/Ladder/ChainBound.lean and Lean4LPD/Pauli/LayerError.lean: there every block starts from a reset state, and merging the last inflow into the chain produces the shifted slot sum over chain (k+1). The present file is the simpler, globally sampled variant, kept as a general theorem next to ChainBound.lean.

Main results

• MultiLadder.majorant_eq_sum_range: the outer sum of the majorant truncates at m + 1, uniformly in the number of layers.
• MultiLadder.sum_steps_le: the bound on the globally sampled mass.

theorem Lean4LPD.MultiLadder.majorant_eq_sum_range {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} {M : ℝ} {m : ℕ} (hm : 1 ≤ m) (T : ℕ) : majorant eps E M m T = M * ∑ k ∈ Finset.range (m + 1), ↑(T.choose k) * chain eps E k m

The outer sum of majorant truncates at m + 1 uniformly in T, which is what lets the sum over Trotter steps be exchanged with it. Both directions vanish: terms with k > m have chain = 0 (a path to rung m cannot use more than m jumps), and terms with k > T have C(T,k) = 0 (there are not enough layers).

theorem Lean4LPD.MultiLadder.sum_steps_le {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} {M : ℝ} (L : MultiLadder eps E M) (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (hM : 0 ≤ M) {G : ℕ} (hG : 1 ≤ G) {m : ℕ} (hm : 1 ≤ m) (r : ℕ) : ∑ d ∈ Finset.range r, L.N m ((d + 1) * G) ≤ M * ∑ k ∈ Finset.range (m + 1), ((↑r + 1) * ↑G) ^ (k + 1) / (↑G * ↑(k + 1).factorial) * chain eps E k m

The globally sampled abstract ladder mass over r blocks.

∑_{d=1}^{r} N_{≥m}^{(dΓ)} ≤ ‖O‖ · ∑_{k≤m} [((r+1)Γ)^{k+1} / (Γ·(k+1)!)] · chain_k^{(m)}.

Each ingredient is a theorem already proved rather than an estimate made here: MultiLadder.le_majorant for the per-block bound, majorant_eq_sum_range to make the outer sum uniform (it needs no sign hypotheses at all — both vanishings are structural), and the slot count Lean4LPD.sum_choose_mul_le for the sum over blocks. Γ is a positive integer, as appropriate for a number of layers.

The sum has the same structure as the sum over Trotter steps in the proof of apd:thm:one_step_truncation_error, but with the slot count C(dΓ, k) of the accumulated mass where that proof has the shifted count of the per-step inflow; see MultiLadder.sum_block_inflow_le for the latter. A separate identification is needed before interpreting this abstract mass as discarded error.