Error Bounds for Orthonormalization

This file records the scalar estimates which compare the intermediate error terms in the proof of the orthonormalization theorem with the paper's final 100 * ζ ^ (1/4) envelope.

Scalar estimates

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.ErrorBounds.orthonormalizationMainLemmaError_two_mul_le_orthonormalizationError (ζ : Error) (hζ : 0 ≤ ζ) : orthonormalizationMainLemmaError (2 * ζ) ≤ orthonormalizationError ζ

Bookkeeping for the submeasurement version of the orthonormalization theorem: after completing A by a fresh outcome, the local measurement lemma returns the error 84·(2ζ)^{1/4}, which is bounded by the paper's 100·ζ^{1/4}.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.ErrorBounds.completionRouteError_bound (ζ : Error) (hζ : 0 ≤ ζ) : orthonormalizationMainLemmaError (consistencyToAlmostProjectiveError (2 * ζ)) ≤ orthonormalizationCompletionRouteError ζ

Error bound for the completion-route proof of the orthonormalization theorem. The completion step gives a 2ζ self-consistency estimate; converting this to a source-almost-projective estimate doubles the scalar to 4ζ, and applying the local 84·ζ^{1/4} repair bound then gives the named envelope orthonormalizationCompletionRouteError ζ.

theorem MIPStarRE.LDT.MakingMeasurementsProjective.Orthonormalization.ErrorBounds.orthonormalizationMainLemmaError_le_orthonormalizationError (ζ : Error) (hζ : 0 ≤ ζ) : orthonormalizationMainLemmaError ζ ≤ orthonormalizationError ζ

The scalar weakening 84·ζ^{1/4} ≤ 100·ζ^{1/4} from the local orthonormalization bound to the paper's error term. Factored out as a named lemma because the same bookkeeping reappears in any top-level theorem that derives orthonormalization from orthonormalizationMeasurement via submeasurement completion.