Error cascade — bounds for σ and ζ₁

This module proves the tight and absorbing bounds for the first two cascade variables, σ and ζ₁. The later variables ζ₂, ζ₃, and ζ₄, together with the top-level consolidator errorCascade_le_mainFormalError, are in the subsequent leaves of Test.MainTheorem.ScalarBounds.CascadeBounds.

The first cascade steps have three components:

• The tight cascade bound (cascadeSigma_tight_bound, cascadeZeta1_bound, …), deriving the native estimate directly from the cascade definition.
• The absorbing bound (sigma_bound, zeta1_bound, …), coarsening the tight estimate to the final mainFormalEnvelope envelope.
• The corresponding nonnegativity lemmas (cascadeSigma_nonneg, cascadeZeta1_nonneg), used by the later cascade estimates.

References

• references/ldt-paper/inductive_step.tex, lines 187–234.

theorem MIPStarRE.LDT.Test.cascadeSigma_tight_bound {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) : cascadeSigma params k ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 1024 80000

theorem MIPStarRE.LDT.Test.sigma_bound {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) : cascadeSigma params k ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 4 * mainFormalEnvelope params k eps

Paper lines 189–193. The paper's bound for σ is absorbed by 10000 · k² · m⁴ · mainFormalEnvelope.

theorem MIPStarRE.LDT.Test.cascadeSigma_nonneg {params : Parameters} {k : ℕ} {ν : Error} (hνNN : 0 ≤ ν) : 0 ≤ cascadeSigma params k ν

theorem MIPStarRE.LDT.Test.cascadeZeta1_nonneg {params : Parameters} {k : ℕ} {eps ν : Error} (h : CascadeHypotheses params k eps) (hνNN : 0 ≤ ν) : 0 ≤ cascadeZeta1 params eps (cascadeSigma params k ν)

theorem MIPStarRE.LDT.Test.cascadeZeta1_bound_special {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) (hkm1 : k = 1 ∧ params.m = 1) : cascadeZeta1 params eps (cascadeSigma params k ν) ≤ 20204 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 2048 160000

theorem MIPStarRE.LDT.Test.cascadeZeta1_bound_general {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) (hkm1 : ¬(k = 1 ∧ params.m = 1)) : cascadeZeta1 params eps (cascadeSigma params k ν) ≤ 20204 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 2048 160000

theorem MIPStarRE.LDT.Test.cascadeZeta1_bound {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) : cascadeZeta1 params eps (cascadeSigma params k ν) ≤ 20204 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 2048 160000

theorem MIPStarRE.LDT.Test.zeta1_bound {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) {ν σ : Error} (hν : ν ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))) (hσEq : σ = cascadeSigma params k ν) : cascadeZeta1 params eps σ ≤ mainFormalError params k eps

Paper lines 196–201. The concrete ζ₁ built from σ = cascadeSigma params k ν is absorbed by mainFormalError.