Error cascade — bound for ζ₄ #
This module contains the ζ₄ cascade estimate used in Step 8 of the main
inductive step and its absorption into mainFormalError.
References #
references/ldt-paper/inductive_step.tex, lines 220--228.
theorem
MIPStarRE.LDT.Test.cascadeZeta4_bound
{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)))
:
cascadeZeta4 (cascadeSigma params k ν) (cascadeZeta1 params eps (cascadeSigma params k ν))
(cascadeZeta3 (cascadeZeta1 params eps (cascadeSigma params k ν))
(cascadeZeta2 (cascadeZeta1 params eps (cascadeSigma params k ν)))) ≤ 40000 * ↑k ^ 2 * ↑params.m ^ 4 * stepEnvelope params k eps 32768 2560000
theorem
MIPStarRE.LDT.Test.zeta4_bound
{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 ζ₁ ζ₂)
:
Paper lines 220–228. The concrete ζ₄ built from the cascade chain is
absorbed by mainFormalError.
theorem
MIPStarRE.LDT.Test.zeta4Repaired_bound
{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 ζ₁ ζ₂)
:
The repaired ζ₄ obtained by substituting the checked local line-169 repair
into the final point-transport triangle is also absorbed by mainFormalError.
Source: This is source-faithful scalar bookkeeping for the repaired
line-169 route documented in docs/paper-gaps/issue-1099-sharper-local-fix.tex
and the final absorption estimate from
references/ldt-paper/inductive_step.tex:186-234.