The last-inflow sum, with the shifted chain index

This file proves the abstract slot-count part of apd:eq:total_high_weight_norm: a bound on the sum over Trotter steps of the mass that flows above the truncation rung during each step, in terms of the chain sums of apd:eq:composition_majorant, and the composition count that bounds those chain sums by binomial coefficients.

The proof of apd:eq:total_high_weight_norm starts from the new inflow during each step, not from a sum of globally accumulated rung norms. Each step starts from a reset state, the mass above the truncation rung having just been discarded, and mass enters only through the per-layer inflow from the lower rungs, which the first-passage majorant bounds. Merging that final jump into the chain gives a chain with one more jump and no extra layer slot: a chain with K jumps carries the slot count C(dΓ, K-1), and the layer of its last jump is accounted for by the prefactor Γ. MultiLadder.sum_steps_le (in Lean4LPD/Ladder/Assembly.lean) bounds a different abstract quantity, with C(dΓ, K), and does not supply an identification with discarded operators.

eps and E stay abstract here: no physical layer estimate, entry-tail estimate or chain-product estimate is assumed. The reset and the per-layer inflow recurrence are explicit hypotheses of block_inflow_le and sum_block_inflow_le; they are proved for the truncated Pauli evolution in Lean4LPD/Pauli/LayerError.lean.

Main results

• MultiLadder.majorant_inflow_eq_shifted_chain: the last inflow of the majorants is the shifted chain sum M · ∑_k C(T,k) · chain (k+1) m.
• MultiLadder.shifted_chain_sum_eq_range: the shifted sum truncates at k < m.
• MultiLadder.sum_inflow_majorant_le: the slot bound for the last-inflow majorants summed over the steps.
• MultiLadder.block_inflow_le, MultiLadder.sum_block_inflow_le: the same bounds for any within-step mass obeying the reset and the per-layer inflow recurrence.
• sum_reverse_choose: the reversed hockey-stick count.
• chain_le_weighted_choose: the composition count, chain (k+1) m ≤ C · R^{m-(k+1)} · W m · C(m-1, k).

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

Merging the final inflow with apd:eq:composition_majorant gives a chain with one more jump and no extra layer slot: the algebraic merge in apd:eq:total_high_weight_norm.

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

The merged chains in apd:eq:total_high_weight_norm have at most m jumps. This cuts the shifted slot sum to k < m uniformly in the layer count T.

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

The last-inflow majorants summed over steps satisfy the shifted slot count of apd:eq:total_high_weight_norm: the outside Γ cancels the slot-bound denominator, leaving exponent K and factorial K! for the chain with K = k+1 jumps.

theorem Lean4LPD.MultiLadder.block_inflow_le {eps : ℕ → ℕ → ℝ} {E : ℕ → ℝ} {M : ℝ} (L : MultiLadder eps E M) (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (hM : 0 ≤ M) {m T G : ℕ} (x : ℕ → ℝ) (hreset : x 0 = 0) (hinflow : ∀ i < G, x (i + 1) ≤ x i + ∑ j ∈ Finset.Ico 1 m, eps j m * L.N (m - j) (T + i) + E m * M) : x G ≤ ↑G * (∑ j ∈ Finset.Ico 1 m, eps j m * majorant eps E M (m - j) (T + G) + E m * M)

Iterate the per-layer inflow from a reset state over the G layers of a block, as in the first step of apd:eq:total_high_weight_norm. Only the majorant, not the lower-rung norms themselves, is moved to the end of the block (majorant_mono). The local recurrence hinflow and the reset hreset must be supplied by the model.

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

The reset-and-layer-inflow route to the merged-chain bound of apd:eq:total_high_weight_norm. x d i is the within-step mass before the final cut; its reset and per-layer recurrence are explicit premises, not an assumed end-to-end truncation bound.

theorem Lean4LPD.sum_reverse_choose {m : ℕ} (hm : 1 ≤ m) (k : ℕ) : ∑ j ∈ Finset.Ico 1 m, ↑((m - j - 1).choose k) = ↑((m - 1).choose (k + 1))

The reversed hockey-stick count ∑_{j=1}^{m-1} C(m-j-1, k) = C(m-1, k+1), used to sum over the final jump in apd:eq:composition_majorant and obtain the composition count in apd:eq:total_high_weight_norm.

theorem Lean4LPD.chain_le_weighted_choose {eps : ℕ → ℕ → ℝ} {E W : ℕ → ℝ} {C R : ℝ} (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hC : 0 ≤ C) (hR : 0 ≤ R) (hentry : ∀ (m : ℕ), 1 ≤ m → E m ≤ C * R ^ (m - 1) * W m) (hjump : ∀ (j m : ℕ), 1 ≤ j → j < m → eps j m * W (m - j) ≤ R ^ (j - 1) * W m) (k m : ℕ) : 1 ≤ m → chain eps E (k + 1) m ≤ C * R ^ (m - (k + 1)) * W m * ↑((m - 1).choose k)

The composition-count part of apd:eq:total_high_weight_norm:

chain ε E (k+1) m ≤ C · R^{m-(k+1)} · W m · C(m-1, k).

Local jump ratios cost at most R^(j-1), while the entry estimate carries C exactly once; summing the recursively defined chains gives the binomial count, rather than assuming that count. The weight function W and its local ratio estimates remain explicit model inputs.