Absorbing restriction loss into the introspection error profile

Restriction multiplies the QLD failure by a fixed edge count. The finite-game argument also needs a budget for the original failure. These lemmas absorb both changes into constants independent of the verifier index and strategy error.

theorem MIPRE.Introspection.self_le_errorProfile_scaled {a b c x ε : ℝ} (ha : 1 ≤ a) (hb0 : 0 ≤ b) (hb1 : b ≤ 1) (hc : 1 ≤ c) (hx : 1 ≤ x) (hε0 : 0 ≤ ε) (hε1 : ε ≤ 1) : ε ≤ errorProfile a b x (c * ε)

On the unit interval, the normalized error profile dominates the original failure, even after increasing that failure by a fixed restriction factor.

theorem MIPRE.Introspection.one_le_errorProfile {a b x ε : ℝ} (ha : 1 ≤ a) (hb : 0 ≤ b) (hx : 1 ≤ x) (hε : 1 ≤ ε) : 1 ≤ errorProfile a b x ε

The normalized profile is already at least one above the unit interval.

theorem MIPRE.Introspection.errorProfile_of_restricted_bound {C a b c x ε δ v : ℝ} (k : ℕ) (hC : 0 ≤ C) (ha : 1 ≤ a) (hb0 : 0 < b) (hb1 : b ≤ 1) (hc : 1 ≤ c) (hx : 1 ≤ x) (hε : 0 ≤ ε) (hδ : δ ≤ errorProfile a b x (c * ε)) (hv : 0 ≤ v) (hvalue : 1 - C * iteratedRoot k (max ε δ) ≤ v) : 1 - errorProfile (powerCoefficient (C * max 1 (c ^ b) ^ rootExponent k) a (rootExponent k)) (b * rootExponent k) x ε ≤ v

A fixed restriction factor and the original-failure budget can both be absorbed into the two-term profile. The large-error case uses only v ≥ 0.