Documentation

MIPRE.Foundations.Introspection.AdaptiveStageBudget

One common quantitative budget for the adaptive stage #

The three actual-test estimates share one budget. The malformed-answer contribution is included in the marginal constant. The replacement loss has three square roots, and the same recurrence can be used at every level.

source
def MIPRE.Introspection.adaptiveStageBudget (r : ℕ) (e z h : ℝ) :
ℝ

e is ordered-edge count times game failure; z and h are the primitive Z and fixed hiding errors. r is the remaining CL depth.

Equations
Instances For
    source
    theorem MIPRE.Introspection.adaptiveStageBudget_nonneg (r : ℕ) {e z h : ℝ} (he : 0 ≤ e) (hz : 0 ≤ z) (hh : 0 ≤ h) :
    0 ≤ adaptiveStageBudget r e z h
    source
    theorem MIPRE.Introspection.marginal_le_adaptiveStageBudget (r : ℕ) {e z h : ℝ} (he : 0 ≤ e) (hz : 0 ≤ z) (hh : 0 ≤ h) :
    16 * z + 56 * e ≤ adaptiveStageBudget r e z h
    source
    theorem MIPRE.Introspection.Z_le_adaptiveStageBudget (r : ℕ) {e z h : ℝ} (he : 0 ≤ e) (hh : 0 ≤ h) :
    64 * z + 224 * e ≤ adaptiveStageBudget r e z h
    source
    theorem MIPRE.Introspection.X_le_adaptiveStageBudget (r : ℕ) {e z h : ℝ} (he : 0 ≤ e) (hz : 0 ≤ z) :
    16 * ((32 * ↑r ^ 2 + 6) * e + 4 * h) ≤ adaptiveStageBudget r e z h
    source
    noncomputable def MIPRE.Introspection.adaptiveStepLoss (δ : ℝ) :
    ℝ

    The exact game-value loss from mixing, common-ancilla dilation, and projective measurement replacement.

    Equations
    Instances For
      source
      theorem MIPRE.Introspection.adaptiveStepLoss_nonneg (δ : ℝ) :
      0 ≤ adaptiveStepLoss δ
      source
      theorem MIPRE.Introspection.adaptiveStepLoss_mono {δ η : ℝ} (h : δ ≤ η) :
      adaptiveStepLoss δ ≤ adaptiveStepLoss η
      source
      theorem MIPRE.Introspection.adaptiveStepLoss_le_root (δ : ℝ) :
      adaptiveStepLoss δ ≤ 8 * iteratedRoot 3 δ

      One replacement costs at most eight times the third iterated square root of the common stage budget, with a universal coefficient.

      source
      noncomputable def MIPRE.Introspection.adaptiveFailureBudget (r : ℕ) (edges z h initial : ℝ) :
      ℕ → ℝ

      An explicit failure recurrence with fixed primitive errors. It records the loss from each replacement; constructing the strategies is separate.

      Equations
      Instances For
        source
        theorem MIPRE.Introspection.adaptiveFailureBudget_step (r n : ℕ) (edges z h initial : ℝ) :
        adaptiveFailureBudget r edges z h initial (n + 1) = adaptiveFailureBudget r edges z h initial n + adaptiveStepLoss (adaptiveStageBudget r (edges * adaptiveFailureBudget r edges z h initial n) z h)
        source
        theorem MIPRE.Introspection.adaptiveFailureBudget_mono (r : ℕ) (edges z h initial : ℝ) :
        Monotone (adaptiveFailureBudget r edges z h initial)