Error cascade — core definitions #
This module defines the central error quantities mainFormalError,
mainFormalEnvelope, the cascade variables σ, ζ₁, ζ₂, ζ₃, ζ₄,
and the CascadeHypotheses numeric regime used throughout the error-cascade
bookkeeping for Step 8 of mainFormal.
Note: this module contributes declarations to the comparator statement closure
of mainFormal, which must elaborate in the same environment as the
Mathlib-only Challenge.lean. Keep the full import Mathlib; do not narrow
it. See docs/comparator.md, "Environment alignment".
References #
references/ldt-paper/inductive_step.tex, lines 187–234.
The formal final error envelope for thm:main-formal.
The sharper pre-completion line-169 repair keeps the point-transport scale at
the original 1/40000 exponent used by the surrounding Step 8 cascade.
Equations
- One or more equations did not get rendered due to their size.
Instances For
At the zero-sampling boundary the displayed final-theorem error collapses to
zero because the envelope carries an explicit factor k^2.
This is the scalar reason that the printed hypothesis k ≥ md does not by
itself supply the nonzero branch of the present final-theorem proof when
d = 0 and k = 0.
The polynomial-exponent envelope common to all cascade bounds,
ε^(1/40000) + (d/q)^(1/40000) + exp(-k/(2560000 m²)). See
mainFormalError_eq_envelope for the identification
mainFormalError = 100000 · k² · m⁴ · mainFormalEnvelope.
Equations
Instances For
mainFormalError factors as 100000 · k² · m⁴ · mainFormalEnvelope.
The envelope is nonnegative whenever ε ≥ 0.
Paper quantity σ (see inductive_step.tex:189), built from an incoming
induction-step error ν and the main-induction exponential decay factor.
Equations
Instances For
Paper quantity ζ₁ = 2σ + 2·√(3ε + 2σ) + m·d/q (see inductive_step.tex:133).
Equations
Instances For
Formal Step 6 quantity
ζ₂ = 200·ζ₁^(1/4) + 42·ζ₁^(1/8).
The paper prints coefficient 40 in inductive_step.tex:149; the extra 2
absorbs the residual + 2ζ₁ term from completing an orthonormalized
submeasurement when 0 ≤ ζ₁ ≤ 1.
Equations
Instances For
Paper quantity ζ₃ = 6·ζ₁ + 6·ζ₂ (see inductive_step.tex:158).
Equations
- MIPStarRE.LDT.Test.cascadeZeta3 ζ₁ ζ₂ = 6 * ζ₁ + 6 * ζ₂
Instances For
Repaired line-169 error obtained by the checked local pre-completion route.
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 used in references/ldt-paper/inductive_step.tex:167-173.
Paper line 169 is printed with the exact error ζ₁; the checked local repair
instead yields ζ₁ + 10·ζ₁^(1/8). The additional term comes from
sqrt (orthonormalizationError ζ₁) = sqrt (100·ζ₁^(1/4)) = 10·ζ₁^(1/8) in
ProjectivizationLine169Repair.leftConsistency_with_orthonormalization_loss
and its Bob-side mirror.
This is an internal repaired-route scalar for the Step 6 transport. It is not
the paper's printed line-169 parameter, and it is later absorbed into
mainFormalError.
Instances For
Repaired final point-consistency scalar obtained by substituting the checked line-169 repair error into the last Step 8 transport triangle.
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 absorbed by the error cascade from
references/ldt-paper/inductive_step.tex:186-234.
The paper's ζ₄ at references/ldt-paper/inductive_step.tex:181 is
2σ + 2·√(ζ₁ + ζ₃/2). This repaired variant replaces ζ₁ by the internal
checked line-169 repair error above, so it is likewise an internal scalar that
is subsequently absorbed into mainFormalError rather than a new paper-facing
theorem parameter.
Equations
- MIPStarRE.LDT.Test.cascadeZeta4Repaired σ ζ₁ ζ₃ = 2 * σ + 2 * √(MIPStarRE.LDT.Test.cascadeLine169RepairError ζ₁ + ζ₃ / 2)
Instances For
Paper origin: references/ldt-paper/inductive_step.tex:130-211
(\label{eq:G-self-consistency} through
\label{eq:final-right-point-consistency}, error cascade ζ₁–ζ₄); blueprint
\label{def:main-formal-error-cascade}.
Source: This is a faithful encoding of the standing scalar regime used in
the paper's error cascade, with the corrected large-(k) and nonzero-sampling
boundaries documented in docs/paper-gaps/issue-906-main-formal-k-bound.tex
and docs/paper-gaps/issue-422-main-formal-zero-k-boundary.tex.
Standing numeric regime used throughout the cascade bounds: parameters
satisfy the unit scale, and ε, d/q ∈ [0, 1].
Instances For
Non-negativity of d/q under the standing hypotheses.
d/q ≤ 1 under the standing hypotheses.
The envelope is nonneg.
1 ≤ m².
1 ≤ k².
1 ≤ m⁴.
m² ≤ m⁴.
k ≤ k².
m ≤ m⁴.
k m² ≤ k² m⁴.
k² · m⁴ ≥ 1.