A positive small-error threshold for every adaptive stage

The failure recurrence has an explicit inverse threshold. For any fixed depth and number of replacements, sufficiently small initial and primitive errors keep every common stage budget at most one. The construction uses the proved triple-square-root replacement loss; no stage-smallness premise is built into the threshold.

theorem MIPRE.Introspection.adaptiveStageBudget_mono_depth {r s : ℕ} (hrs : r ≤ s) {e z h : ℝ} (he : 0 ≤ e) : adaptiveStageBudget r e z h ≤ adaptiveStageBudget s e z h

theorem MIPRE.Introspection.adaptiveStageBudget_mono_errors (r : ℕ) {e e' z z' h h' : ℝ} (he : e ≤ e') (hz : z ≤ z') (hh : h ≤ h') : adaptiveStageBudget r e z h ≤ adaptiveStageBudget r e' z' h'

theorem MIPRE.Introspection.adaptiveFailureBudget_nonneg (r n : ℕ) (edges z h : ℝ) {initial : ℝ} (hi : 0 ≤ initial) : 0 ≤ adaptiveFailureBudget r edges z h initial n

def MIPRE.Introspection.adaptiveBudgetCoefficient (r : ℕ) (edges : ℝ) : ℝ

A coefficient controlling the whole stage when its three error inputs are all at most the same number.

Equations

• MIPRE.Introspection.adaptiveBudgetCoefficient r edges = (512 * ↑r ^ 2 + 224) * edges + 128

theorem MIPRE.Introspection.adaptiveBudgetCoefficient_pos (r : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 0 < adaptiveBudgetCoefficient r edges

theorem MIPRE.Introspection.adaptiveStageBudget_le_coefficient (r : ℕ) {edges f z h t : ℝ} (hE : 0 ≤ edges) (hf : f ≤ t) (hz : z ≤ t) (hh : h ≤ t) : adaptiveStageBudget r (edges * f) z h ≤ adaptiveBudgetCoefficient r edges * t

theorem MIPRE.Introspection.iteratedRoot_three_pow_eight {t : ℝ} (ht : 0 ≤ t) : iteratedRoot 3 (t ^ 8) = t

A stack of three square roots exactly inverts the eighth power on nonnegative inputs.

def MIPRE.Introspection.adaptiveSmallThreshold (r : ℕ) (edges : ℝ) : ℕ → ℝ

Explicit inverse thresholds. The half-size term controls the old failure and the eighth-power term controls the new replacement loss.

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.adaptiveSmallThreshold r edges 0 = 1 / MIPRE.Introspection.adaptiveBudgetCoefficient r edges

theorem MIPRE.Introspection.adaptiveSmallThreshold_pos (r n : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 0 < adaptiveSmallThreshold r edges n

theorem MIPRE.Introspection.adaptiveSmallThreshold_antitone (r : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : Antitone (adaptiveSmallThreshold r edges)

theorem MIPRE.Introspection.adaptiveFailure_step_le_threshold (r n : ℕ) {edges f z h : ℝ} (hE : 0 ≤ edges) (hf : f ≤ adaptiveSmallThreshold r edges (n + 1)) (hz : z ≤ adaptiveSmallThreshold r edges (n + 1)) (hh : h ≤ adaptiveSmallThreshold r edges (n + 1)) : f + adaptiveStepLoss (adaptiveStageBudget r (edges * f) z h) ≤ adaptiveSmallThreshold r edges n

One actual numerical recurrence step consumes exactly one inverse threshold level. In particular, this is derived from the replacement loss formula, rather than requiring the desired next bound as a hypothesis.

theorem MIPRE.Introspection.adaptiveFailureBudget_le_threshold (r N : ℕ) {edges z h initial : ℝ} (hE : 0 ≤ edges) (hi : initial ≤ adaptiveSmallThreshold r edges N) (hz : z ≤ adaptiveSmallThreshold r edges N) (hh : h ≤ adaptiveSmallThreshold r edges N) (n : ℕ) : n ≤ N → adaptiveFailureBudget r edges z h initial n ≤ adaptiveSmallThreshold r edges (N - n)

If all three initial errors fit the depth-N threshold, the failure after n replacements fits the threshold with N-n levels remaining.

theorem MIPRE.Introspection.adaptiveStageBudget_le_one_of_threshold (r N : ℕ) {edges z h initial : ℝ} (hE : 0 ≤ edges) (hi : initial ≤ adaptiveSmallThreshold r edges N) (hz : z ≤ adaptiveSmallThreshold r edges N) (hh : h ≤ adaptiveSmallThreshold r edges N) (n : ℕ) (hn : n ≤ N) : adaptiveStageBudget r (edges * adaptiveFailureBudget r edges z h initial n) z h ≤ 1

An explicit sufficient condition for every stage budget required by a finite adaptive iteration, including the final numerical bound.