Power bounds for the full finite adaptive recurrence

Each replacement introduces three square roots. For any fixed number of replacements the actual failure recurrence is bounded by an explicit constant times the corresponding iterated root of a common primitive error. A second explicit coefficient makes this bound at least one outside the proved admissible small-error regime. These numerical statements do not assume the existence or soundness of the strategy construction.

theorem MIPRE.Introspection.iteratedRoot_nonneg (n : ℕ) {t : ℝ} (ht : 0 ≤ t) : 0 ≤ iteratedRoot n t

theorem MIPRE.Introspection.iteratedRoot_pos (n : ℕ) {t : ℝ} (ht : 0 < t) : 0 < iteratedRoot n t

theorem MIPRE.Introspection.iteratedRoot_mono (n : ℕ) : Monotone (iteratedRoot n)

theorem MIPRE.Introspection.iteratedRoot_one (n : ℕ) : iteratedRoot n 1 = 1

theorem MIPRE.Introspection.iteratedRoot_le_one (n : ℕ) {t : ℝ} (ht : t ≤ 1) : iteratedRoot n t ≤ 1

theorem MIPRE.Introspection.iteratedRoot_add (m n : ℕ) (t : ℝ) : iteratedRoot (m + n) t = iteratedRoot m (iteratedRoot n t)

theorem MIPRE.Introspection.self_le_iteratedRoot (n : ℕ) {t : ℝ} (ht0 : 0 ≤ t) (ht1 : t ≤ 1) : t ≤ iteratedRoot n t

theorem MIPRE.Introspection.sqrt_scale_le {c t : ℝ} (hc : 1 ≤ c) : √(c * t) ≤ c * √t

theorem MIPRE.Introspection.iteratedRoot_scale_le (n : ℕ) {c t : ℝ} (hc : 1 ≤ c) : iteratedRoot n (c * t) ≤ c * iteratedRoot n t

A coefficient at least one can be kept unchanged through any fixed stack of square roots, which is convenient for explicit uniform constants.

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

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

The coefficient accumulated per replacement in a simple power bound.

Equations

• MIPRE.Introspection.adaptivePowerCoefficient r edges = 1 + 8 * MIPRE.Introspection.adaptiveBudgetCoefficient r edges

theorem MIPRE.Introspection.adaptivePowerCoefficient_one_le (r : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 1 ≤ adaptivePowerCoefficient r edges

theorem MIPRE.Introspection.adaptiveFailureBudget_le_power (r n : ℕ) {edges z h initial t : ℝ} (hE : 0 ≤ edges) (ht0 : 0 ≤ t) (ht1 : t ≤ 1) (hi : initial ≤ t) (hz : z ≤ t) (hh : h ≤ t) : adaptiveFailureBudget r edges z h initial n ≤ adaptivePowerCoefficient r edges ^ n * iteratedRoot (3 * n) t

The actual finite recurrence has exponent 8^(-n). This estimate has no stage-admissibility premise and works for any fixed number of steps, including two full local iterations.

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

noncomputable def MIPRE.Introspection.adaptiveSoundnessCoefficient (r : ℕ) (edges : ℝ) (n : ℕ) : ℝ

This fixed coefficient also pays for the trivial probability bound outside the admissible regime. The denominator is strictly positive.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.adaptiveSoundnessCoefficient_one_le (r n : ℕ) {edges : ℝ} (hE : 0 ≤ edges) : 1 ≤ adaptiveSoundnessCoefficient r edges n

theorem MIPRE.Introspection.adaptiveFailureBudget_le_soundness_power (r n : ℕ) {edges z h initial t : ℝ} (hE : 0 ≤ edges) (ht0 : 0 ≤ t) (ht : t ≤ adaptiveSmallThreshold r edges n) (hi : initial ≤ t) (hz : z ≤ t) (hh : h ≤ t) : adaptiveFailureBudget r edges z h initial n ≤ adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) t

theorem MIPRE.Introspection.one_le_soundness_power_of_threshold_le (r n : ℕ) {edges t : ℝ} (hE : 0 ≤ edges) (ht : adaptiveSmallThreshold r edges n ≤ t) : 1 ≤ adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) t

If the common input error exceeds the explicit admissible threshold, the same soundness power bound is at least one.

theorem MIPRE.Introspection.adaptiveSoundness_power_cases (r n : ℕ) {edges z h initial t : ℝ} (hE : 0 ≤ edges) (ht0 : 0 ≤ t) (hi : initial ≤ t) (hz : z ≤ t) (hh : h ≤ t) : t ≤ adaptiveSmallThreshold r edges n ∧ adaptiveFailureBudget r edges z h initial n ≤ adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) t ∨ 1 ≤ adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) t

The full numerical dichotomy for any finite number of replacements: either the original admissibility threshold holds and the actual recurrence is bounded, or the very same power bound makes probability loss vacuous.

theorem MIPRE.Introspection.adaptiveSoundness_power_le_errorProfile (r n : ℕ) {edges a b x ε : ℝ} (hE : 0 ≤ edges) (ha : 0 ≤ a) (hx : 1 ≤ x) (hε : 0 ≤ ε) : adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) (errorProfile a b x ε) ≤ errorProfile (powerCoefficient (adaptiveSoundnessCoefficient r edges n) a (rootExponent (3 * n))) (b * rootExponent (3 * n)) x ε

The uniform power controlling both numerical regimes has exactly the paper's required two-term profile after fixed-power absorption.

theorem MIPRE.Introspection.exists_adaptiveSoundness_errorProfile (r n : ℕ) {edges a b : ℝ} (hE : 0 ≤ edges) (ha : 0 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) : ∃ (a' : ℝ) (b' : ℝ), 1 ≤ a' ∧ 0 < b' ∧ b' ≤ 1 ∧ ∀ (x ε : ℝ), 1 ≤ x → 0 ≤ ε → adaptiveSoundnessCoefficient r edges n * iteratedRoot (3 * n) (errorProfile a b x ε) ≤ errorProfile a' b' x ε

Constants for the final soundness profile depend only on fixed depth, edge count, number of replacements, and the primitive profile constants.