The product estimate and the quantitative D-sector assembly

This file completes the scalar part of the proof of apd:eq:total_high_weight_norm. It bounds the rung product by a factorial times a power, sums the slot polynomial over the sectors of chains with D = m - K fewer jumps than the all-ones chain, and assembles the result into the c₀ form of apd:eq:c0.

The product estimate

By prod_rungW_eq the rung product is ∏_{j=2}^{n+1} w_j = (k_h-1)^n ∏_{i=1}^{n} (i+c), and prod_add_one_le_factorial_exp_rpow bounds ∏_{i=1}^{n} (i+c) by n! (e n)^c. The shifted product ∏_{j=2}^{n+1} (j+c) dominates it termwise (prod_shift_le), and prod_shifted_le_factorial_exp_rpow proves the corresponding estimate (n+1)! (e(n+1))^c for the shifted product as well, so the estimate is available in either indexing.

The assembly

total_truncation_error_product_bound composes total_truncation_error with the product estimate and retains its hypothesis hstep explicitly. The later theorems prove the factorial/exponential sector estimate, combine it with the reset/local-inflow lemmas of Lean4LPD/Ladder/ChainBound.lean, and use Lean4LPD/Constants/ChainWeights.lean to discharge the concrete jump and entry bounds. The final theorem MultiLadder.sum_block_epsJump_le_cZero concludes the c₀-form scalar bound, which is the shape of hstep, from reset and local layer inflow. It is a statement about an abstract MultiLadder; the Pauli trajectory, its reset and its layer inflow are supplied in Lean4LPD/Pauli/LayerError.lean.

Main results

• prod_add_one_le_factorial_exp_rpow, prod_shifted_le_factorial_exp_rpow: the product estimate in the two indexings.
• total_truncation_error_product_bound: total_truncation_error with the product estimate applied.
• sum_factorial_sectors_le_exp, slot_polynomial_le_exp: the D-sector sum is bounded by an exponential.
• chain_slot_sum_le_exp, MultiLadder.sum_block_inflow_le_exp: the sector estimate combined with the composition count and with the block-inflow bound.
• cZero_pow_nat, sector_bound_le_cZero: the passage to the c₀ form.
• MultiLadder.sum_block_epsJump_le_cZero: the c₀-form bound for the concrete jump norms.

theorem Lean4LPD.prod_add_one_le_factorial_exp_rpow {c : ℝ} (hc : 0 ≤ c) (n : ℕ) (hn : 1 ≤ n) : ∏ i ∈ Finset.range n, (↑i + 1 + c) ≤ ↑n.factorial * (Real.exp 1 * ↑n) ^ c

The product estimate for apd:eq:total_high_weight_norm: for c ≥ 0 and n ≥ 1, ∏_{i=1}^n (i+c) ≤ n! (e n)^c. By prod_rungW_eq the left-hand side is the rung product ∏_{j=2}^{n+1} w_j up to the factor (k_h-1)^n. The proof writes the product as n! ∏_{i=1}^n (1 + c/i), bounds it by n! exp(c H_n), and uses H_n ≤ 1 + log n.

The hypothesis n ≥ 1 cannot be dropped: at n = 0 the empty product is 1, while (e · 0)^c = 0 for every c > 0.

theorem Lean4LPD.prod_shifted_le_factorial_exp_rpow {c : ℝ} (hc : 0 ≤ c) (n : ℕ) : ∏ i ∈ Finset.range n, (↑i + 2 + c) ≤ ↑(n + 1).factorial * (Real.exp 1 * (↑n + 1)) ^ c

The product estimate for apd:eq:total_high_weight_norm in shifted indexing: ∏_{j=2}^{n+1} (j+c) ≤ (n+1)! (e(n+1))^c for c ≥ 0 and every n. Since 1 + c ≥ 1, the shifted product over n factors is at most the unshifted product over n + 1 factors, so this follows from prod_add_one_le_factorial_exp_rpow at n + 1.

theorem Lean4LPD.total_truncation_error_product_bound {S M t a G kh1 c B : ℝ} {m r : ℕ} (hstep : S ≤ ((cZero (↑r) (↑m) G B * G * a * t) ^ (m + 1) * ∏ j ∈ Finset.range (m + 1), rungW kh1 c (j + 2)) / ↑(m + 1).factorial * M) (hadm : Admissible (↑r) (↑m) G) (hm1 : 1 ≤ ↑m) (hr5 : 5 ≤ ↑r) (hB0 : 0 ≤ B) (hB1 : B ≤ 1) (hkh1 : 0 < kh1) (hc : 0 ≤ c) (ha : 0 < a) (ht : 0 ≤ t) (hM : 0 ≤ M) : S ≤ decayBase G (kh1 + 1) a t ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M

total_truncation_error composed with the product estimate prod_add_one_le_factorial_exp_rpow: the summed truncation error is at most (t/t₀)^{m+1} (e(m+1))^c ‖O‖ with t/t₀ = decayBase Γ k_h a t. Only the product estimate is added here; the hypothesis hstep of total_truncation_error is retained unchanged, and is proved from reset and layer inflow in MultiLadder.sum_block_epsJump_le_cZero below.

theorem Lean4LPD.factorial_ratio_le_pow {m D : ℕ} (hD : D ≤ m) : ↑m.factorial / ↑(m - D).factorial ≤ ↑m ^ D

The factorial-ratio estimate m!/(m-D)! ≤ m^D used in apd:eq:total_high_weight_norm, proved through the falling factorial.

theorem Lean4LPD.sum_factorial_sectors_le_exp (m : ℕ) {y : ℝ} (hy : 0 ≤ y) : ∑ D ∈ Finset.range m, ↑((m - 1).choose D) * (↑m.factorial / ↑(m - D).factorial) * y ^ D ≤ Real.exp (↑m ^ 2 * y)

The factorial and composition-count factors in apd:eq:total_high_weight_norm are bounded by the exponential series, for every m at once: ∑_{D<m} C(m-1, D) · m!/(m-D)! · y^D ≤ exp(m² y) for y ≥ 0.

theorem Lean4LPD.slot_polynomial_eq_sectors {m : ℕ} (hm : 1 ≤ m) {X R : ℝ} (hX : 0 < X) : ∑ k ∈ Finset.range m, X ^ (k + 1) / ↑(k + 1).factorial * R ^ (m - (k + 1)) * ↑((m - 1).choose k) = X ^ m / ↑m.factorial * ∑ D ∈ Finset.range m, ↑((m - 1).choose D) * (↑m.factorial / ↑(m - D).factorial) * (R / X) ^ D

Exact reindexing by D=m-K in apd:eq:total_high_weight_norm, keeping the all-ones prefactor X^m/m! explicit. Only the positive slot count X is divided out.

theorem Lean4LPD.slot_polynomial_le_exp {m : ℕ} (hm : 1 ≤ m) {X R : ℝ} (hX : 0 < X) (hR : 0 ≤ R) : ∑ k ∈ Finset.range m, X ^ (k + 1) / ↑(k + 1).factorial * R ^ (m - (k + 1)) * ↑((m - 1).choose k) ≤ X ^ m / ↑m.factorial * Real.exp (R * ↑m ^ 2 / X)

The complete factorial/slot D-sector estimate in apd:eq:total_high_weight_norm, generalized from 9/4 to any nonnegative part-ratio bound R.

theorem Lean4LPD.chain_slot_sum_le_exp {eps : ℕ → ℕ → ℝ} {E W : ℕ → ℝ} {C R X : ℝ} {m : ℕ} (hm : 1 ≤ m) (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hC : 0 ≤ C) (hR : 0 ≤ R) (hW : 0 ≤ W m) (hX : 0 < X) (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 ∈ Finset.range m, X ^ (k + 1) / ↑(k + 1).factorial * chain eps E (k + 1) m ≤ C * W m * X ^ m / ↑m.factorial * Real.exp (R * ↑m ^ 2 / X)

Combine the proved local-ratio chain bound with the full D-sector estimate of apd:eq:total_high_weight_norm. The entry inflation C is charged exactly once; the desired chain sum is a conclusion, not one of the local coefficient hypotheses.

theorem Lean4LPD.MultiLadder.sum_block_inflow_le_exp {eps : ℕ → ℕ → ℝ} {E W : ℕ → ℝ} {M C R : ℝ} (L : MultiLadder eps E M) (heps : ∀ (j m : ℕ), 0 ≤ eps j m) (hE : ∀ (m : ℕ), 0 ≤ E m) (hM : 0 ≤ M) (hC : 0 ≤ C) (hR : 0 ≤ R) {m G : ℕ} (hm : 1 ≤ m) (hG : 1 ≤ G) (hW : 0 ≤ W m) (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) (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) : ∑ d ∈ Finset.range r, x d G ≤ M * (C * W m * ((↑r + 1) * ↑G) ^ m / ↑m.factorial * Real.exp (R * ↑m ^ 2 / ((↑r + 1) * ↑G)))

The abstract reset/local-inflow route through the entire quantitative sector sum of apd:eq:total_high_weight_norm. It still requires a concrete model to supply the local inflow and local coefficient ratios; no final discarded-mass bound is assumed.

theorem Lean4LPD.cZero_pow_nat {r G B : ℝ} (hB : 0 ≤ B) (m : ℕ) : cZero r (↑m) G B ^ (m + 1) = ((r + 1) / r) ^ (m + 1) * Real.exp (9 / 4 * (↑m + 1) ^ 2 / (r * G)) * (1 + B)

Raising c₀ to the power m + 1 recovers the correction factors of apd:eq:c0 exactly: c₀^{m+1} = ((r+1)/r)^{m+1} · exp(9(m+1)²/(4rΓ)) · (1+B). This is an identity, valid for every natural m including m = 0; it does not use the bound c₀ ≤ 2 of cZero_le_two, which requires m ≥ 1 (see two_lt_cZero_of_m_zero).

theorem Lean4LPD.sector_bound_le_cZero {r G B a A P M : ℝ} (hr : 0 < r) (hG : 0 < G) (hB : 0 ≤ B) (ha0 : 0 ≤ a) (hA : 0 ≤ A) (ha : a ≤ A / r) (hP : 0 ≤ P) (hM : 0 ≤ M) (m : ℕ) : M * ((1 + B) * (a ^ (m + 1) * P) * ((r + 1) * G) ^ (m + 1) / ↑(m + 1).factorial * Real.exp (9 / 4 * (↑m + 1) ^ 2 / ((r + 1) * G))) ≤ (cZero r (↑m) G B * G * A) ^ (m + 1) * P / ↑(m + 1).factorial * M

The scalar passage from the sharper sector denominator (r+1)Γ to the c₀ shape of apd:eq:total_high_weight_norm and apd:eq:c0. A stands for the paper's product αt; only the angle bound a ≤ A/r is used.

theorem Lean4LPD.MultiLadder.sum_block_epsJump_le_exp_source {kh1 c a M : ℝ} (L : MultiLadder (epsJump kh1 c a) (entryFactor kh1 c a) M) (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (hb : betaOf kh1 c a ≤ 1 / 2) (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, epsJump kh1 c a j m * L.N (m - j) (d * G + i) + entryFactor kh1 c a m * M) : ∑ d ∈ Finset.range r, x d G ≤ M * ((1 + 4 * Real.exp 1 * betaOf kh1 c a) * chainWeight kh1 c a m * ((↑r + 1) * ↑G) ^ m / ↑m.factorial * Real.exp (9 / 4 * ↑m ^ 2 / ((↑r + 1) * ↑G)))

The concrete epsJump/entryFactor specialization of apd:eq:total_high_weight_norm, with the paper's entry constant 1 + 4eβ. All local coefficient and entry premises are discharged by ChainWeights; only the model's reset and layer-inflow recurrence remain inputs.

theorem Lean4LPD.MultiLadder.sum_block_epsJump_le_cZero {kh1 c a A M : ℝ} (L : MultiLadder (epsJump kh1 c a) (entryFactor kh1 c a) M) (hkh : 0 < kh1) (hc : 0 ≤ c) (ha : 0 ≤ a) (hb : betaOf kh1 c a ≤ 1 / 2) (hA : 0 ≤ A) (hM : 0 ≤ M) {G r : ℕ} (hG : 1 ≤ G) (hr : 1 ≤ r) (haA : a ≤ A / ↑r) (m : ℕ) (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 + 1), epsJump kh1 c a j (m + 1) * L.N (m + 1 - j) (d * G + i) + entryFactor kh1 c a (m + 1) * M) : ∑ d ∈ Finset.range r, x d G ≤ ((cZero (↑r) (↑m) (↑G) (4 * Real.exp 1 * betaOf kh1 c a) * ↑G * A) ^ (m + 1) * ∏ j ∈ Finset.range (m + 1), rungW kh1 c (j + 2)) / ↑(m + 1).factorial * M

The quantitative hstep shape is a conclusion, not a hypothesis. This proves the scalar assembly in apd:eq:total_high_weight_norm / apd:eq:c0 for reset blocks obeying the concrete multi-jump layer recurrence. A Pauli model must still instantiate L, x, their reset, and their local inflow, which Lean4LPD/Pauli/LayerError.lean does; no equality with a post-cut retained mass is assumed. A = αt yields the exact input shape of total_truncation_error.