Main-formal scalar bounds

Scalar estimates for the two-space mainFormal theorem. This module defines the five scalars that appear in the paper's error calculation:

• σ — the symmetrized induction consistency error
• ζ₁ — the cross-consistency error after unsymmetrization
• ζ₂ — the orthonormalize-and-complete closeness error
• ζ₃ — the projective self-consistency error
• ζ₄ — the final point-consistency error

The core structure MainFormalScalarBounds (Prop) bundles the three hypotheses needed to invoke the checked Step 8 bound errorCascade_le_mainFormalError:

• cascadeHypotheses — the standing scalar regime (q > 0, k ≥ 1, m ≥ 1, 0 ≤ ε ≤ 1, d ≤ q).
• inductionNu_nonneg — nonnegativity of the symmetrized main-induction ν at (3ε, 3ε, 3ε).
• inductionNu_bound — the paper line 71–73 coarsening ν ≤ 10000 k² m² (ε^{1/1024} + (d/q)^{1/1024}).

The cascade comparisons ζ₁ ≤ …, ζ₃ ≤ 2·mainFormalError, etc. are then derived in the private theorem cascadeBounds via errorCascade_le_mainFormalError, which calls the already-formalized scalar cascade estimates from LDT.Test.MainTheorem.ScalarBounds. The module also provides the vacuous-branch analysis (mainFormalError_ge_one_of_*) and the coarsening lemma that absorbs orthonormalizeAndCompleteError into ζ₂ (orthonormalizeAndCompleteError_zeta1_le_zeta2).

References

• Paper: references/ldt-paper/inductive_step.tex, error computations (lines 68–75, 186–234).
• Blueprint: blueprint/src/chapter/ch10_induction.tex, \label{def:main-formal-error-cascade}, \label{thm:sigma-bound-main-formal}, and \label{thm:zeta-bounds-main-formal}.

noncomputable def MIPStarRE.LDT.Test.mainFormalInductionNu (params : Parameters) (k : ℕ) (eps : Error) : Error

The Section 3 specialization of the main-induction ν after Step 1 symmetrization.

Paper lines 68--75 apply thm:main-induction to the symmetrized strategy with errors (3ε, 3ε, 3ε) and then coarsen its ν to the Section 3 scalar cascade. This definition keeps the pre-coarsened main-induction quantity available for the main theorem conclusion.

Equations

• MIPStarRE.LDT.Test.mainFormalInductionNu params k eps = MIPStarRE.LDT.MainInductionStep.mainInductionNu params k (3 * eps) (3 * eps) (3 * eps)

theorem MIPStarRE.LDT.Test.mainFormalScalarSigma_eq_mainInductionError (params : Parameters) (k : ℕ) (eps : Error) : cascadeSigma params k (mainFormalInductionNu params k eps) = MainInductionStep.mainInductionError params k (3 * eps) (3 * eps) (3 * eps)

The σ built from mainFormalInductionNu is definitionally the Section 6 main-induction error at (3ε, 3ε, 3ε).

This is the exact scalar handoff between paper lines 75--81 and the cascade notation used from line 133 onward.

theorem MIPStarRE.LDT.Test.mainFormalInductionNu_nonneg {params : Parameters} {k : ℕ} {eps : Error} (h : CascadeHypotheses params k eps) : 0 ≤ mainFormalInductionNu params k eps

Nonnegativity of the symmetrized main-induction ν under the standing cascade hypotheses.

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

Paper lines 71--73: after applying main induction to the symmetrized strategy, the resulting ν at errors (3ε,3ε,3ε) is bounded by the coarser Section 3 quantity 10000 k² m² (ε^(1/1024) + (d/q)^(1/1024)).

theorem MIPStarRE.LDT.Test.mainFormalError_ge_one_of_one_le_envelope (params : Parameters) (k : ℕ) (eps : Error) (hk0 : 0 < k) (henv : 1 ≤ mainFormalEnvelope params k eps) : 1 ≤ mainFormalError params k eps

If the unscaled Step 8 envelope is already at least 1, then the public mainFormalError envelope is also at least 1.

theorem MIPStarRE.LDT.Test.mainFormalError_ge_one_of_one_lt_eps (params : Parameters) (k : ℕ) {eps : Error} (hk0 : 0 < k) (heps : 1 < eps) : 1 ≤ mainFormalError params k eps

If ε > 1, then the final error envelope has already saturated past 1. This discharges the non-paper regime before invoking the paper's Step 8 cascade, which assumes ε ≤ 1.

theorem MIPStarRE.LDT.Test.mainFormalError_ge_one_of_q_lt_d (params : Parameters) (k : ℕ) (eps : Error) (hk0 : 0 < k) (hepsNN : 0 ≤ eps) (hqd : ↑params.q < ↑params.d) : 1 ≤ mainFormalError params k eps

If d > q, then the final error envelope has already saturated past 1. Thus the nontrivial Step 8 branch may assume the paper's ambient d/q ≤ 1 regime.

theorem MIPStarRE.LDT.Test.cascadeHypotheses_of_not_mainFormalError_ge_one {params : Parameters} {k : ℕ} {eps : Error} (hepsNN : 0 ≤ eps) (hk0 : 0 < k) (hsmall : ¬1 ≤ mainFormalError params k eps) : CascadeHypotheses params k eps

In the non-vacuous branch of mainFormal, the standing scalar hypotheses of Step 8 follow from the theorem's basic positivity data.

Source: This is source-faithful scalar bookkeeping for references/ldt-paper/inductive_step.tex:186-234, under the corrected 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.

If either ε > 1 or d > q, the final error mainFormalError is already at least 1, so mainFormal_trivial_witness handles the theorem. Hence under ¬ 1 ≤ mainFormalError params k eps we may safely enter the paper's cascade regime 0 ≤ ε ≤ 1 and d/q ≤ 1.

structure MIPStarRE.LDT.Test.MainFormalScalarBounds (params : Parameters) (eps : Error) (k : ℕ) : Prop

Scalar hypotheses for the Section 3 error cascade of mainFormal.

This record is intentionally scalar-only. It does not assert any measurement transport. Its fields are precisely the hypotheses needed to invoke the already formalized Step 8 bound errorCascade_le_mainFormalError on the main-induction ν produced after symmetrization (paper lines 68--75). The corrected source route derives these scalar side conditions in the non-vacuous branch and otherwise uses the saturated-error witness.

• cascadeHypotheses : CascadeHypotheses params k eps

  Standing scalar regime for the paper's cascade estimates.

• inductionNu_nonneg : 0 ≤ mainFormalInductionNu params k eps

  Nonnegativity of the main-induction ν at (3ε, 3ε, 3ε).

• inductionNu_bound : mainFormalInductionNu params k eps ≤ 10000 * ↑k ^ 2 * ↑params.m ^ 2 * (Real.rpow eps (1 / 1024) + Real.rpow (↑params.d / ↑params.q) (1 / 1024))

  Paper line 71--73 coarsening of the main-induction ν.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.ofCascadeHypotheses {params : Parameters} {eps : Error} {k : ℕ} (h : CascadeHypotheses params k eps) : MainFormalScalarBounds params eps k

Build the scalar data once the standing cascade hypotheses hold; the main-induction ν nonnegativity and paper line 71--73 coarsening are discharged by the checked scalar lemmas above.

Source: This is a source-faithful constructor for the scalar regime in references/ldt-paper/inductive_step.tex:68-75 and references/ldt-paper/inductive_step.tex:186-234.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.ofNontrivialMainFormal {params : Parameters} {eps : Error} {k : ℕ} (hepsNN : 0 ≤ eps) (hk0 : 0 < k) (hsmall : ¬1 ≤ mainFormalError params k eps) : MainFormalScalarBounds params eps k

Build the scalar data in the non-vacuous branch of mainFormal.

The branch hypothesis ¬ 1 ≤ mainFormalError params k eps rules out the non-paper regimes ε > 1 and d > q, while hepsNN and hk0 supply the remaining scalar positivity hypotheses.

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.sigma {params : Parameters} {eps : Error} {k : ℕ} (_scalars : MainFormalScalarBounds params eps k) : Error

The paper's σ, built from the symmetrized main-induction ν.

Equations

• _scalars.sigma = MIPStarRE.LDT.Test.cascadeSigma params k (MIPStarRE.LDT.Test.mainFormalInductionNu params k eps)

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta1 {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The paper's ζ₁ = 2σ + 2√(3ε + 2σ) + md/q.

Equations

• scalars.zeta1 = MIPStarRE.LDT.Test.cascadeZeta1 params eps scalars.sigma

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta2 {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The formal Step 6 scalar ζ₂ = 200ζ₁^(1/4) + 42ζ₁^(1/8), widening the paper's printed coefficient 40 to absorb the extra completion term.

Equations

• scalars.zeta2 = MIPStarRE.LDT.Test.cascadeZeta2 scalars.zeta1

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta3 {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The paper's self-consistency scalar ζ₃ = 6ζ₁ + 6ζ₂.

Equations

• scalars.zeta3 = MIPStarRE.LDT.Test.cascadeZeta3 scalars.zeta1 scalars.zeta2

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta4 {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The paper's point-consistency scalar ζ₄ = 2σ + 2√(ζ₁ + ζ₃/2).

Equations

• scalars.zeta4 = MIPStarRE.LDT.Test.cascadeZeta4 scalars.sigma scalars.zeta1 scalars.zeta3

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.line169Error {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The repaired line-169 error ζ₁ + 10·ζ₁^(1/8) coming from the checked local pre-completion transport.

Equations

• scalars.line169Error = MIPStarRE.LDT.Test.cascadeLine169RepairError scalars.zeta1

noncomputable def MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta4Repaired {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : Error

The repaired point-consistency scalar obtained by substituting the checked line-169 repair error into the final point-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 paper's final cascade estimate in references/ldt-paper/inductive_step.tex:186-234.

Equations

• scalars.zeta4Repaired = MIPStarRE.LDT.Test.cascadeZeta4Repaired scalars.sigma scalars.zeta1 scalars.zeta3

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.sigma_nonneg {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : 0 ≤ scalars.sigma

Nonnegativity of the native cascade σ.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta1_nonneg {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : 0 ≤ scalars.zeta1

Nonnegativity of the native cascade ζ₁.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta1_le_mainFormalError {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : scalars.zeta1 ≤ mainFormalError params k eps

Step 8 absorption for the native ζ₁ target.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta1_le_one_of_not_mainFormalError_ge_one {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) (hsmall : ¬1 ≤ mainFormalError params k eps) : scalars.zeta1 ≤ 1

In the non-vacuous branch, the cascade scalar ζ₁ lies in the unit interval.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.orthonormalizeAndCompleteError_zeta1_le_zeta2 {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) (hsmall : ¬1 ≤ mainFormalError params k eps) : MakingMeasurementsProjective.orthonormalizeAndCompleteError scalars.zeta1 ≤ scalars.zeta2

The formal ζ₂ scalar absorbs the literal Step 6 orthonormalize-and-complete error in the non-vacuous branch.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta4Repaired_le_mainFormalError {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : scalars.zeta4Repaired ≤ mainFormalError params k eps

Step 8 absorption for the repaired ζ₄ point-consistency targets.

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.

theorem MIPStarRE.LDT.Test.MainFormalScalarBounds.zeta3_div_two_le_mainFormalError {params : Parameters} {eps : Error} {k : ℕ} (scalars : MainFormalScalarBounds params eps k) : scalars.zeta3 / 2 ≤ mainFormalError params k eps

Step 8 absorption for the native ζ₃/2 self-consistency target.