Error cascade — final assembly #
This module contains the final tuple-valued consolidator for the error cascade in Step 8 of the main inductive step.
References #
references/ldt-paper/inductive_step.tex, lines 230--234.
theorem
MIPStarRE.LDT.Test.errorCascade_le_mainFormalError
{params : Parameters}
{k : ℕ}
{eps : Error}
(h : CascadeHypotheses params k eps)
{ν σ ζ₁ ζ₂ ζ₃ : Error}
(hνNN : 0 ≤ ν)
(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 ν)
(hζ₁Eq : ζ₁ = cascadeZeta1 params eps σ)
(hζ₂Eq : ζ₂ = cascadeZeta2 ζ₁)
(hζ₃Eq : ζ₃ = cascadeZeta3 ζ₁ ζ₂)
:
σ ≤ mainFormalError params k eps ∧ ζ₁ ≤ mainFormalError params k eps ∧ ζ₂ ≤ mainFormalError params k eps ∧ ζ₃ ≤ 2 * mainFormalError params k eps ∧ cascadeZeta4 σ ζ₁ ζ₃ ≤ mainFormalError params k eps
Paper lines 230--234. Packages the five cascade bounds into the tuple
used by mainFormal.