Norm-level cutoff existence

This file proves the existence form of apd:thm:truncation_threshold_entangled at norm level: for a decay base 0 ≤ q < 1, the majorant q^(m+1) (e(m+1))^c M supplied by total_truncation_error_product_bound tends to zero in the rung m, so every sufficiently large rung m ≥ 1 brings it below any tolerance ε > 0.

Main results

• norm_majorant_tendsto_zero: q^(m+1) (e(m+1))^c M → 0 as m → ∞, for 0 ≤ q < 1.
• exists_eventual_norm_threshold, exists_norm_threshold: a rung m ≥ 1 meeting the tolerance exists, and so does every larger rung.
• exists_uniform_norm_threshold, exists_uniform_weight_cutoff: one rung, respectively one weight cutoff w = k_o + (k_h − 1)m, for a whole family sharing the same q, c, M.
• exists_model_norm_threshold: the case q = decayBase G kh α t with t < tZeroModel G kh α.
• exists_admissible_step_count: a step count r can be chosen after the rung.

Scope

apd:thm:truncation_threshold_entangled and eq:truncation_weight_bound use exponential decay to dominate the polynomial factor. Here the norm-level majorant q^(m+1) (e(m+1))^c M tends to zero when 0 ≤ q < 1; for c ≥ 0 its factor (e(m+1))^c is smaller than the factor (m*+2)(e(m*+2))^c of apd:eq:total_truncation_error. The analytic limit permits any real c, M; physical applications use the nonnegative constants supplied by the norm bound. Mathlib's real-power/exponential asymptotic is reused directly.

The conclusions are cutoff existence, a conservative form of the paper's corollary: the explicit logarithmic/log-log estimate of m*, the runtime statement (apd:thm:runtime) and the conversion to an error in expectation are not formalized here. The uniform-family corollary requires one common q,c,M bound for the entire family; dimension independence is not inferred when those parameters, especially the observable norm bound, grow with dimension. Converting a uniform rung to a uniform weight also requires fixed k_o,k_h; the weight corollary keeps these outside the family quantifier explicitly.

Choosing a larger numerical step count is separate from constructing the corresponding gate angles. Nothing here assumes a fixed angle family still satisfies a ≤ αt/r after r changes.

theorem Lean4LPD.norm_majorant_tendsto_zero {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (c M : ℝ) : Filter.Tendsto (fun (m : ℕ) => q ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M) Filter.atTop (nhds 0)

The analytic decay behind apd:thm:truncation_threshold_entangled, applied to the norm-level majorant of total_truncation_error_product_bound: for 0 ≤ q < 1 and all real c, M, q^(m+1) (e(m+1))^c M → 0 as m → ∞. The exponential decay of q^(m+1) dominates the polynomial factor.

theorem Lean4LPD.exists_eventual_norm_threshold {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (c M : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (m₀ : ℕ), 1 ≤ m₀ ∧ ∀ (m : ℕ), m₀ ≤ m → q ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M ≤ ε

Every sufficiently large natural rung meets the norm tolerance, the existence part of apd:thm:truncation_threshold_entangled. No explicit logarithmic formula for the rung is asserted, and no hypothesis on the input state is involved.

theorem Lean4LPD.exists_norm_threshold {q : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (c M : ℝ) {ε : ℝ} (hε : 0 < ε) : ∃ (m : ℕ), 1 ≤ m ∧ q ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M ≤ ε

A natural cutoff rung satisfying the requested absolute norm tolerance, from apd:thm:truncation_threshold_entangled at norm level only.

theorem Lean4LPD.exists_uniform_norm_threshold {ι : Type u_1} {error : ι → ℕ → ℝ} {q c M : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (hbound : ∀ (i : ι) (m : ℕ), 1 ≤ m → error i m ≤ q ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M) {ε : ℝ} (hε : 0 < ε) : ∃ (m₀ : ℕ), 1 ≤ m₀ ∧ ∀ (m : ℕ), m₀ ≤ m → ∀ (i : ι), error i m ≤ ε

The cutoff can be chosen independently of the family index when the same q,c,M majorizes the whole family. This is the qualified dimension-independent interpretation of apd:thm:truncation_threshold_entangled, for absolute norm tolerance.

theorem Lean4LPD.exists_uniform_weight_cutoff {ι : Type u_1} {error : ι → ℕ → ℝ} {q c M : ℝ} (hq0 : 0 ≤ q) (hq1 : q < 1) (ko kh : ℕ) (hbound : ∀ (i : ι) (m : ℕ), 1 ≤ m → error i (ko + (kh - 1) * m) ≤ q ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M) {ε : ℝ} (hε : 0 < ε) : ∃ (w : ℕ) (m : ℕ), 1 ≤ m ∧ w = ko + (kh - 1) * m ∧ ∀ (i : ι), error i w ≤ ε

A single weight cutoff works for the whole family when k_o,k_h,q,c,M are all fixed uniform data. This is the norm-level, absolute-tolerance form of eq:truncation_weight_bound, not a runtime or expectation theorem.

theorem Lean4LPD.exists_model_norm_threshold {G kh α t c M ε : ℝ} (hG : 0 < G) (hkh : 1 < kh) (hα : 0 < α) (ht : 0 ≤ t) (htime : t < tZeroModel G kh α) (hε : 0 < ε) : ∃ (m : ℕ), 1 ≤ m ∧ decayBase G kh α t ^ (m + 1) * (Real.exp 1 * (↑m + 1)) ^ c * M ≤ ε

The model-only short-time condition t < tZeroModel G kh α supplies 0≤q<1 for q = decayBase G kh α t, so the norm-level cutoff exists. This is the model-threshold counterpart of apd:thm:truncation_threshold_entangled; it concerns the norm-level majorant only, so no hypothesis on the input state is involved.

theorem Lean4LPD.exists_admissible_step_count (m : ℕ) (B₁ B₂ : ℝ) : ∃ (r : ℕ), 5 ≤ r ∧ m ≤ r ∧ B₁ ≤ ↑r ∧ B₂ ≤ ↑r

Numerical step counts can be chosen after the rung: an Archimedean helper for the conditions of apd:eq:multijump_factor. The two real lower bounds B₁, B₂ may encode the paper's finite-step conditions r ≥ 8(m*+1)²/Γ and r ≥ 8e²·w₂·αt; satisfying them does not construct or update any gate-angle family.